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	|- ( ( A e. C /\ B e. D ) -> { A } ~~ { B } )

Proof

Step	Hyp	Ref	Expression
1		snex	|- { <. A , B >. } e. _V
2		f1osng	|- ( ( A e. C /\ B e. 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 >. } e. _V -> ( { <. A , B >. } : { A } -1-1-onto-> { B } -> E. f f : { A } -1-1-onto-> { B } ) )
5	1 2 4	mpsyl	|- ( ( A e. C /\ B e. D ) -> E. f f : { A } -1-1-onto-> { B } )
6		bren	|- ( { A } ~~ { B } <-> E. f f : { A } -1-1-onto-> { B } )
7	5 6	sylibr	|- ( ( A e. C /\ B e. D ) -> { A } ~~ { B } )