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

Proof

Step Hyp Ref Expression
1 ssequn2 A B B A = B
2 undif1 B A A = B A
3 2 eqeq1i B A A = B B A = B
4 1 3 bitr4i A B B A A = B