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 ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → { 𝐴 } ≈ { 𝐵 } )

Proof

Step Hyp Ref Expression
1 snex ⊢ { ⟨ 𝐴 , 𝐵 ⟩ } ∈ V
2 f1osng ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → { ⟨ 𝐴 , 𝐵 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐵 } )
3 f1oeq1 ⊢ ( 𝑓 = { ⟨ 𝐴 , 𝐵 ⟩ } → ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐵 } ↔ { ⟨ 𝐴 , 𝐵 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐵 } ) )
4 3 spcegv ⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ } ∈ V → ( { ⟨ 𝐴 , 𝐵 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐵 } → ∃ 𝑓 𝑓 : { 𝐴 } –1-1-onto→ { 𝐵 } ) )
5 1 2 4 mpsyl ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ∃ 𝑓 𝑓 : { 𝐴 } –1-1-onto→ { 𝐵 } )
6 snex ⊢ { 𝐴 } ∈ V
7 snex ⊢ { 𝐵 } ∈ V
8 breng ⊢ ( ( { 𝐴 } ∈ V ∧ { 𝐵 } ∈ V ) → ( { 𝐴 } ≈ { 𝐵 } ↔ ∃ 𝑓 𝑓 : { 𝐴 } –1-1-onto→ { 𝐵 } ) )
9 6 7 8 mp2an ⊢ ( { 𝐴 } ≈ { 𝐵 } ↔ ∃ 𝑓 𝑓 : { 𝐴 } –1-1-onto→ { 𝐵 } )
10 5 9 sylibr ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → { 𝐴 } ≈ { 𝐵 } )