Metamath Proof Explorer

Theorem difun2

Description: Absorption of union by difference. Theorem 36 of Suppes p. 29. (Contributed by NM, 19-May-1998)

Ref Expression
Assertion difun2 
|- ( ( A u. B ) \ B ) = ( A \ B )

Proof

Step Hyp Ref Expression
1 difundir 
 |-  ( ( A u. B ) \ B ) = ( ( A \ B ) u. ( B \ B ) )
2 difid 
 |-  ( B \ B ) = (/)
3 2 uneq2i 
 |-  ( ( A \ B ) u. ( B \ B ) ) = ( ( A \ B ) u. (/) )
4 un0 
 |-  ( ( A \ B ) u. (/) ) = ( A \ B )
5 1 3 4 3eqtri 
 |-  ( ( A u. B ) \ B ) = ( A \ B )