Metamath Proof Explorer


Theorem undifr

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

Ref Expression
Assertion undifr A B B A A = B

Proof

Step Hyp Ref Expression
1 undif A B A B A = B
2 uncom A B A = B A A
3 2 eqeq1i A B A = B B A A = B
4 1 3 bitri A B B A A = B