Metamath Proof Explorer

Theorem djueq2

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

Ref Expression
Assertion djueq2 
|- ( A = B -> ( C |_| A ) = ( C |_| B ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  C = C
2 djueq12 
 |-  ( ( C = C /\ A = B ) -> ( C |_| A ) = ( C |_| B ) )
3 1 2 mpan 
 |-  ( A = B -> ( C |_| A ) = ( C |_| B ) )