Theorem en2sn

Description: Two singletons are equinumerous. (Contributed by NM, 9-Nov-2003) Avoid ax-pow . (Revised by BTernaryTau, 31-Jul-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		bren	⊢ ( { 𝐴 } ≈ { 𝐵 } ↔ ∃ 𝑓 𝑓 : { 𝐴 } –1-1-onto→ { 𝐵 } )
7	5 6	sylibr	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → { 𝐴 } ≈ { 𝐵 } )