Metamath Proof Explorer

Theorem undifr

Description: Union of complementary parts into whole. (Contributed by Thierry Arnoux, 21-Nov-2023) (Proof shortened by SN, 11-Mar-2025)

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

Proof

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