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 
|- ( ( 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 } )