Metamath Proof Explorer

Theorem invdif

Description: Intersection with universal complement. Remark in Stoll p. 20. (Contributed by NM, 17-Aug-2004)

Ref Expression
Assertion invdif 
|- ( A i^i ( _V \ B ) ) = ( A \ B )

Proof

Step Hyp Ref Expression
1 dfin2 
 |-  ( A i^i ( _V \ B ) ) = ( A \ ( _V \ ( _V \ B ) ) )
2 ddif 
 |-  ( _V \ ( _V \ B ) ) = B
3 2 difeq2i 
 |-  ( A \ ( _V \ ( _V \ B ) ) ) = ( A \ B )
4 1 3 eqtri 
 |-  ( A i^i ( _V \ B ) ) = ( A \ B )