This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfun3

Description: Union defined in terms of intersection (De Morgan's law). Definition of union in Mendelson p. 231. (Contributed by NM, 8-Jan-2002)

Ref Expression
Assertion dfun3 ⊢ A ∪ B = V ∖ V ∖ A ∩ V ∖ B

Proof

Step Hyp Ref Expression
1 dfun2 ⊢ A ∪ B = V ∖ V ∖ A ∖ B
2 dfin2 ⊢ V ∖ A ∩ V ∖ B = V ∖ A ∖ V ∖ V ∖ B
3 ddif ⊢ V ∖ V ∖ B = B
4 3 difeq2i ⊢ V ∖ A ∖ V ∖ V ∖ B = V ∖ A ∖ B
5 2 4 eqtr2i ⊢ V ∖ A ∖ B = V ∖ A ∩ V ∖ B
6 5 difeq2i ⊢ V ∖ V ∖ A ∖ B = V ∖ V ∖ A ∩ V ∖ B
7 1 6 eqtri ⊢ A ∪ B = V ∖ V ∖ A ∩ V ∖ B