Metamath Proof Explorer

Theorem undif

Description: Union of complementary parts into whole. (Contributed by NM, 22-Mar-1998)

Ref Expression
Assertion undif 
|- ( A C_ B <-> ( A u. ( B \ A ) ) = B )

Proof

Step Hyp Ref Expression
1 ssequn1 
 |-  ( A C_ B <-> ( A u. B ) = B )
2 undif2 
 |-  ( A u. ( B \ A ) ) = ( A u. B )
3 2 eqeq1i 
 |-  ( ( A u. ( B \ A ) ) = B <-> ( A u. B ) = B )
4 1 3 bitr4i 
 |-  ( A C_ B <-> ( A u. ( B \ A ) ) = B )