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 i^i B ) = ( _V \ ( ( _V \ A ) u. ( _V \ B ) ) )

Proof

Step Hyp Ref Expression
1 ddif 
 |-  ( _V \ ( _V \ ( A \ ( _V \ B ) ) ) ) = ( A \ ( _V \ B ) )
2 dfun2 
 |-  ( ( _V \ A ) u. ( _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 ) u. ( _V \ B ) ) = ( _V \ ( A \ ( _V \ B ) ) )
7 6 difeq2i 
 |-  ( _V \ ( ( _V \ A ) u. ( _V \ B ) ) ) = ( _V \ ( _V \ ( A \ ( _V \ B ) ) ) )
8 dfin2 
 |-  ( A i^i B ) = ( A \ ( _V \ B ) )
9 1 7 8 3eqtr4ri 
 |-  ( A i^i B ) = ( _V \ ( ( _V \ A ) u. ( _V \ B ) ) )