Theorem djueq12

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

	Ref	Expression
Assertion	djueq12	$$⊢\left(A=B\wedge C=D\right)\to \left(A\mathrm{\bigsqcup ︀}C\right)=\left(B\mathrm{\bigsqcup ︀}D\right)$$

Proof

Step	Hyp	Ref	Expression
1		xpeq2	$$⊢A=B\to \left\{\varnothing \right\}\times A=\left\{\varnothing \right\}\times B$$
2	1	adantr	$$⊢\left(A=B\wedge C=D\right)\to \left\{\varnothing \right\}\times A=\left\{\varnothing \right\}\times B$$
3		xpeq2	$$⊢C=D\to \left\{1_{𝑜}\right\}\times C=\left\{1_{𝑜}\right\}\times D$$
4	3	adantl	$$⊢\left(A=B\wedge C=D\right)\to \left\{1_{𝑜}\right\}\times C=\left\{1_{𝑜}\right\}\times D$$
5	2 4	uneq12d	$$⊢\left(A=B\wedge C=D\right)\to \left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times C\right)=\left(\left\{\varnothing \right\}\times B\right)\cup \left(\left\{1_{𝑜}\right\}\times D\right)$$
6		df-dju	$$⊢\left(A\mathrm{\bigsqcup ︀}C\right)=\left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times C\right)$$
7		df-dju	$$⊢\left(B\mathrm{\bigsqcup ︀}D\right)=\left(\left\{\varnothing \right\}\times B\right)\cup \left(\left\{1_{𝑜}\right\}\times D\right)$$
8	5 6 7	3eqtr4g	$$⊢\left(A=B\wedge C=D\right)\to \left(A\mathrm{\bigsqcup ︀}C\right)=\left(B\mathrm{\bigsqcup ︀}D\right)$$