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 ∖ 𝐵 ) ) )