Metamath Proof Explorer

Theorem difabs

Description: Absorption-like law for class difference: you can remove a class only once. (Contributed by FL, 2-Aug-2009)

Ref Expression
Assertion difabs 
|- ( ( A \ B ) \ B ) = ( A \ B )

Proof

Step Hyp Ref Expression
1 difun1 
 |-  ( A \ ( B u. B ) ) = ( ( A \ B ) \ B )
2 unidm 
 |-  ( B u. B ) = B
3 2 difeq2i 
 |-  ( A \ ( B u. B ) ) = ( A \ B )
4 1 3 eqtr3i 
 |-  ( ( A \ B ) \ B ) = ( A \ B )