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 ( 𝐴 ∩ 𝐵 ) = ( V ∖ ( ( V ∖ 𝐴 ) ∪ ( V ∖ 𝐵 ) ) )

Proof

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