Let X, A and B be given.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ X ∖ (A ∪ B).
We will prove x ∈ (X ∖ A) ∩ (X ∖ B).
We prove the intermediate claim Hxpair: x ∈ X ∧ x ∉ (A ∪ B).
An exact proof term for the current goal is (setminusE X (A ∪ B) x Hx).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (andEL (x ∈ X) (x ∉ (A ∪ B)) Hxpair).
We prove the intermediate claim HxNot: x ∉ (A ∪ B).
An exact proof term for the current goal is (andER (x ∈ X) (x ∉ (A ∪ B)) Hxpair).
We prove the intermediate claim HxNotA: x ∉ A.
Assume HxA: x ∈ A.
We prove the intermediate claim HxAB: x ∈ A ∪ B.
An exact proof term for the current goal is (binunionI1 A B x HxA).
An exact proof term for the current goal is (HxNot HxAB).
We prove the intermediate claim HxNotB: x ∉ B.
Assume HxB: x ∈ B.
We prove the intermediate claim HxAB: x ∈ A ∪ B.
An exact proof term for the current goal is (binunionI2 A B x HxB).
An exact proof term for the current goal is (HxNot HxAB).
An exact proof term for the current goal is (binintersectI (X ∖ A) (X ∖ B) x (setminusI X A x HxX HxNotA) (setminusI X B x HxX HxNotB)).
Let x be given.
Assume Hx: x ∈ (X ∖ A) ∩ (X ∖ B).
We will prove x ∈ X ∖ (A ∪ B).
We prove the intermediate claim HxXA: x ∈ X ∖ A.
An exact proof term for the current goal is (binintersectE1 (X ∖ A) (X ∖ B) x Hx).
We prove the intermediate claim HxXB: x ∈ X ∖ B.
An exact proof term for the current goal is (binintersectE2 (X ∖ A) (X ∖ B) x Hx).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X A x HxXA).
We prove the intermediate claim HxNotA: x ∉ A.
An exact proof term for the current goal is (setminusE2 X A x HxXA).
We prove the intermediate claim HxNotB: x ∉ B.
An exact proof term for the current goal is (setminusE2 X B x HxXB).
We prove the intermediate claim HxNotAB: x ∉ (A ∪ B).
Assume HxAB: x ∈ A ∪ B.
Apply (binunionE A B x HxAB) to the current goal.
Assume HxA.
An exact proof term for the current goal is (HxNotA HxA).
Assume HxB.
An exact proof term for the current goal is (HxNotB HxB).
An exact proof term for the current goal is (setminusI X (A ∪ B) x HxX HxNotAB).
∎