Metamath Proof Explorer

Theorem f1oeng

Description: The domain and range of a one-to-one, onto function are equinumerous. (Contributed by NM, 19-Jun-1998)

Ref Expression
Assertion f1oeng 
|- ( ( A e. C /\ F : A -1-1-onto-> B ) -> A ~~ B )

Proof

Step Hyp Ref Expression
1 fornex 
 |-  ( A e. C -> ( F : A -onto-> B -> B e. _V ) )
2 f1ofo 
 |-  ( F : A -1-1-onto-> B -> F : A -onto-> B )
3 1 2 impel 
 |-  ( ( A e. C /\ F : A -1-1-onto-> B ) -> B e. _V )
4 f1oen2g 
 |-  ( ( A e. C /\ B e. _V /\ F : A -1-1-onto-> B ) -> A ~~ B )
5 4 3com23 
 |-  ( ( A e. C /\ F : A -1-1-onto-> B /\ B e. _V ) -> A ~~ B )
6 3 5 mpd3an3 
 |-  ( ( A e. C /\ F : A -1-1-onto-> B ) -> A ~~ B )