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

Metamath Proof Explorer

Theorem dfin3

Description: Intersection defined in terms of union (De Morgan's law). Similar to Exercise 4.10(n) of Mendelson p. 231. (Contributed by NM, 8-Jan-2002)

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

Proof

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