Metamath Proof Explorer

Theorem f1oen

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

Ref Expression
Hypothesis f1oen.1 
|- A e. _V
Assertion f1oen 
|- ( F : A -1-1-onto-> B -> A ~~ B )

Proof

Step Hyp Ref Expression
1 f1oen.1 
 |-  A e. _V
2 f1oeng 
 |-  ( ( A e. _V /\ F : A -1-1-onto-> B ) -> A ~~ B )
3 1 2 mpan 
 |-  ( F : A -1-1-onto-> B -> A ~~ B )