djueq12

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

		Ref	Expression
	Assertion	djueq12	$⊢ (A = B \land C = D) \to (A ⊔︀ C) = (B ⊔︀ D)$

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

Metamath Proof Explorer