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 ≈ B ∧ C ≈ D ∧ B ∩ D = ∅ → A ⊔︀ C ≈ B ∪ D

Proof

Step Hyp Ref Expression
1 djuen ⊢ A ≈ B ∧ C ≈ D → A ⊔︀ C ≈ B ⊔︀ D
2 1 3adant3 ⊢ A ≈ B ∧ C ≈ D ∧ B ∩ D = ∅ → A ⊔︀ C ≈ B ⊔︀ D
3 relen ⊢ Rel ⁡ ≈
4 3 brrelex2i ⊢ A ≈ B → B ∈ V
5 3 brrelex2i ⊢ C ≈ D → D ∈ V
6 id ⊢ B ∩ D = ∅ → B ∩ D = ∅
7 endjudisj ⊢ B ∈ V ∧ D ∈ V ∧ B ∩ D = ∅ → B ⊔︀ D ≈ B ∪ D
8 4 5 6 7 syl3an ⊢ A ≈ B ∧ C ≈ D ∧ B ∩ D = ∅ → B ⊔︀ D ≈ B ∪ D
9 entr ⊢ A ⊔︀ C ≈ B ⊔︀ D ∧ B ⊔︀ D ≈ B ∪ D → A ⊔︀ C ≈ B ∪ D
10 2 8 9 syl2anc ⊢ A ≈ B ∧ C ≈ D ∧ B ∩ D = ∅ → A ⊔︀ C ≈ B ∪ D