Metamath Proof Explorer


Theorem undifr

Description: Union of complementary parts into whole. (Contributed by Thierry Arnoux, 21-Nov-2023)

Ref Expression
Assertion undifr ( 𝐴𝐵 ↔ ( ( 𝐵𝐴 ) ∪ 𝐴 ) = 𝐵 )

Proof

Step Hyp Ref Expression
1 undif ( 𝐴𝐵 ↔ ( 𝐴 ∪ ( 𝐵𝐴 ) ) = 𝐵 )
2 uncom ( 𝐴 ∪ ( 𝐵𝐴 ) ) = ( ( 𝐵𝐴 ) ∪ 𝐴 )
3 2 eqeq1i ( ( 𝐴 ∪ ( 𝐵𝐴 ) ) = 𝐵 ↔ ( ( 𝐵𝐴 ) ∪ 𝐴 ) = 𝐵 )
4 1 3 bitri ( 𝐴𝐵 ↔ ( ( 𝐵𝐴 ) ∪ 𝐴 ) = 𝐵 )