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