Metamath Proof Explorer

Theorem undifabs

Description: Absorption of difference by union. (Contributed by NM, 18-Aug-2013)

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

Proof

Step Hyp Ref Expression
1 undif3 
 |-  ( A u. ( A \ B ) ) = ( ( A u. A ) \ ( B \ A ) )
2 unidm 
 |-  ( A u. A ) = A
3 2 difeq1i 
 |-  ( ( A u. A ) \ ( B \ A ) ) = ( A \ ( B \ A ) )
4 difdif 
 |-  ( A \ ( B \ A ) ) = A
5 1 3 4 3eqtri 
 |-  ( A u. ( A \ B ) ) = A