This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem en2sn

Description: Two singletons are equinumerous. (Contributed by NM, 9-Nov-2003) Avoid ax-pow . (Revised by BTernaryTau, 31-Jul-2024) Avoid ax-un . (Revised by BTernaryTau, 25-Sep-2024)

Ref Expression
Assertion en2sn ⊢ A ∈ C ∧ B ∈ D → A ≈ B

Proof

Step Hyp Ref Expression
1 snex ⊢ A B ∈ V
2 f1osng ⊢ A ∈ C ∧ B ∈ D → A B : A ⟶ 1-1 onto B
3 f1oeq1 ⊢ f = A B → f : A ⟶ 1-1 onto B ↔ A B : A ⟶ 1-1 onto B
4 3 spcegv ⊢ A B ∈ V → A B : A ⟶ 1-1 onto B → ∃ f f : A ⟶ 1-1 onto B
5 1 2 4 mpsyl ⊢ A ∈ C ∧ B ∈ D → ∃ f f : A ⟶ 1-1 onto B
6 snex ⊢ A ∈ V
7 snex ⊢ B ∈ V
8 breng ⊢ A ∈ V ∧ B ∈ V → A ≈ B ↔ ∃ f f : A ⟶ 1-1 onto B
9 6 7 8 mp2an ⊢ A ≈ B ↔ ∃ f f : A ⟶ 1-1 onto B
10 5 9 sylibr ⊢ A ∈ C ∧ B ∈ D → A ≈ B