Metamath Proof Explorer

Theorem dfun2

Description: An alternate definition of the union of two classes in terms of class difference, requiring no dummy variables. Along with dfin2 and dfss4 it shows we can express union, intersection, and subset directly in terms of the single "primitive" operation \ (class difference). (Contributed by NM, 10-Jun-2004)

Ref Expression
Assertion dfun2 ⊢ A ∪ B = V ∖ V ∖ A ∖ B

Proof

Step Hyp Ref Expression
1 vex ⊢ x ∈ V
2 eldif ⊢ x ∈ V ∖ A ↔ x ∈ V ∧ ¬ x ∈ A
3 1 2 mpbiran ⊢ x ∈ V ∖ A ↔ ¬ x ∈ A
4 3 anbi1i ⊢ x ∈ V ∖ A ∧ ¬ x ∈ B ↔ ¬ x ∈ A ∧ ¬ x ∈ B
5 eldif ⊢ x ∈ V ∖ A ∖ B ↔ x ∈ V ∖ A ∧ ¬ x ∈ B
6 ioran ⊢ ¬ x ∈ A ∨ x ∈ B ↔ ¬ x ∈ A ∧ ¬ x ∈ B
7 4 5 6 3bitr4i ⊢ x ∈ V ∖ A ∖ B ↔ ¬ x ∈ A ∨ x ∈ B
8 7 con2bii ⊢ x ∈ A ∨ x ∈ B ↔ ¬ x ∈ V ∖ A ∖ B
9 eldif ⊢ x ∈ V ∖ V ∖ A ∖ B ↔ x ∈ V ∧ ¬ x ∈ V ∖ A ∖ B
10 1 9 mpbiran ⊢ x ∈ V ∖ V ∖ A ∖ B ↔ ¬ x ∈ V ∖ A ∖ B
11 8 10 bitr4i ⊢ x ∈ A ∨ x ∈ B ↔ x ∈ V ∖ V ∖ A ∖ B
12 11 uneqri ⊢ A ∪ B = V ∖ V ∖ A ∖ B