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