Metamath Proof Explorer

Theorem djuenun

Description: Disjoint union is equinumerous to union for disjoint sets. (Contributed by Mario Carneiro, 29-Apr-2015) (Revised by Jim Kingdon, 19-Aug-2023)

		Ref	Expression
	Assertion	djuenun	$⊢ (A \approx B \land C \approx D \land B \cap D = \emptyset) \to (A ⊔︀ C) \approx (B \cup D)$

Proof

Step	Hyp	Ref	Expression
1		djuen	$⊢ (A \approx B \land C \approx D) \to (A ⊔︀ C) \approx (B ⊔︀ D)$
2	1	3adant3	$⊢ (A \approx B \land C \approx D \land B \cap D = \emptyset) \to (A ⊔︀ C) \approx (B ⊔︀ D)$
3		relen	$⊢ Rel \approx$
4	3	brrelex2i	$⊢ A \approx B \to B \in V$
5	3	brrelex2i	$⊢ C \approx D \to D \in V$
6		id	$⊢ B \cap D = \emptyset \to B \cap D = \emptyset$
7		endjudisj	$⊢ (B \in V \land D \in V \land B \cap D = \emptyset) \to (B ⊔︀ D) \approx (B \cup D)$
8	4 5 6 7	syl3an	$⊢ (A \approx B \land C \approx D \land B \cap D = \emptyset) \to (B ⊔︀ D) \approx (B \cup D)$
9		entr	$⊢ ((A ⊔︀ C) \approx (B ⊔︀ D) \land (B ⊔︀ D) \approx (B \cup D)) \to (A ⊔︀ C) \approx (B \cup D)$
10	2 8 9	syl2anc	$⊢ (A \approx B \land C \approx D \land B \cap D = \emptyset) \to (A ⊔︀ C) \approx (B \cup D)$