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

Proof

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