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

Proof

Step Hyp Ref Expression
1 djuen ( ( 𝐴𝐵𝐶𝐷 ) → ( 𝐴𝐶 ) ≈ ( 𝐵𝐷 ) )
2 1 3adant3 ( ( 𝐴𝐵𝐶𝐷 ∧ ( 𝐵𝐷 ) = ∅ ) → ( 𝐴𝐶 ) ≈ ( 𝐵𝐷 ) )
3 relen Rel ≈
4 3 brrelex2i ( 𝐴𝐵𝐵 ∈ V )
5 3 brrelex2i ( 𝐶𝐷𝐷 ∈ V )
6 id ( ( 𝐵𝐷 ) = ∅ → ( 𝐵𝐷 ) = ∅ )
7 endjudisj ( ( 𝐵 ∈ V ∧ 𝐷 ∈ V ∧ ( 𝐵𝐷 ) = ∅ ) → ( 𝐵𝐷 ) ≈ ( 𝐵𝐷 ) )
8 4 5 6 7 syl3an ( ( 𝐴𝐵𝐶𝐷 ∧ ( 𝐵𝐷 ) = ∅ ) → ( 𝐵𝐷 ) ≈ ( 𝐵𝐷 ) )
9 entr ( ( ( 𝐴𝐶 ) ≈ ( 𝐵𝐷 ) ∧ ( 𝐵𝐷 ) ≈ ( 𝐵𝐷 ) ) → ( 𝐴𝐶 ) ≈ ( 𝐵𝐷 ) )
10 2 8 9 syl2anc ( ( 𝐴𝐵𝐶𝐷 ∧ ( 𝐵𝐷 ) = ∅ ) → ( 𝐴𝐶 ) ≈ ( 𝐵𝐷 ) )