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 ABBAA=B

Proof

Step Hyp Ref Expression
1 ssequn2 ABBA=B
2 undif1 BAA=BA
3 2 eqeq1i BAA=BBA=B
4 1 3 bitr4i ABBAA=B