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 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		snex	|- { A } e. _V
7		snex	|- { B } e. _V
8		breng	|- ( ( { A } e. _V /\ { B } e. _V ) -> ( { A } ~~ { B } <-> E. f f : { A } -1-1-onto-> { B } ) )
9	6 7 8	mp2an	|- ( { A } ~~ { B } <-> E. f f : { A } -1-1-onto-> { B } )
10	5 9	sylibr	|- ( ( A e. C /\ B e. D ) -> { A } ~~ { B } )