Metamath Proof Explorer

Theorem djueq1

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

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

Proof

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