Metamath Proof Explorer


Theorem djueq2

Description: Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022)

Ref Expression
Assertion djueq2 A=BC⊔︀A=C⊔︀B

Proof

Step Hyp Ref Expression
1 eqid C=C
2 djueq12 C=CA=BC⊔︀A=C⊔︀B
3 1 2 mpan A=BC⊔︀A=C⊔︀B