Metamath Proof Explorer


Theorem en2snOLD

Description: Obsolete version of en2sn as of 25-Sep-2024. (Contributed by NM, 9-Nov-2003) Avoid ax-pow . (Revised by BTernaryTau, 31-Jul-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion en2snOLD
|- ( ( 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 } )