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 ( ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ) → ( 𝐴 ⊔ 𝐶 ) = ( 𝐵 ⊔ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 xpeq2 ⊢ ( 𝐴 = 𝐵 → ( { ∅ } × 𝐴 ) = ( { ∅ } × 𝐵 ) )
2 1 adantr ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ) → ( { ∅ } × 𝐴 ) = ( { ∅ } × 𝐵 ) )
3 xpeq2 ⊢ ( 𝐶 = 𝐷 → ( { 1o } × 𝐶 ) = ( { 1o } × 𝐷 ) )
4 3 adantl ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ) → ( { 1o } × 𝐶 ) = ( { 1o } × 𝐷 ) )
5 2 4 uneq12d ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ) → ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐶 ) ) = ( ( { ∅ } × 𝐵 ) ∪ ( { 1o } × 𝐷 ) ) )
6 df-dju ⊢ ( 𝐴 ⊔ 𝐶 ) = ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐶 ) )
7 df-dju ⊢ ( 𝐵 ⊔ 𝐷 ) = ( ( { ∅ } × 𝐵 ) ∪ ( { 1o } × 𝐷 ) )
8 5 6 7 3eqtr4g ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ) → ( 𝐴 ⊔ 𝐶 ) = ( 𝐵 ⊔ 𝐷 ) )