This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem djueq12

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

Ref Expression
Assertion djueq12 
|- ( ( A = B /\ C = D ) -> ( A |_| C ) = ( B |_| D ) )

Proof

Step Hyp Ref Expression
1 xpeq2 
 |-  ( A = B -> ( { (/) } X. A ) = ( { (/) } X. B ) )
2 1 adantr 
 |-  ( ( A = B /\ C = D ) -> ( { (/) } X. A ) = ( { (/) } X. B ) )
3 xpeq2 
 |-  ( C = D -> ( { 1o } X. C ) = ( { 1o } X. D ) )
4 3 adantl 
 |-  ( ( A = B /\ C = D ) -> ( { 1o } X. C ) = ( { 1o } X. D ) )
5 2 4 uneq12d 
 |-  ( ( A = B /\ C = D ) -> ( ( { (/) } X. A ) u. ( { 1o } X. C ) ) = ( ( { (/) } X. B ) u. ( { 1o } X. D ) ) )
6 df-dju 
 |-  ( A |_| C ) = ( ( { (/) } X. A ) u. ( { 1o } X. C ) )
7 df-dju 
 |-  ( B |_| D ) = ( ( { (/) } X. B ) u. ( { 1o } X. D ) )
8 5 6 7 3eqtr4g 
 |-  ( ( A = B /\ C = D ) -> ( A |_| C ) = ( B |_| D ) )