Description: The domain and range of a onetoone, onto function are equinumerous. (Contributed by NM, 19Jun1998)
Ref  Expression  

Hypothesis  f1oen.1   A e. _V 

Assertion  f1oen   ( F : A 11onto> B > A ~~ B ) 
Step  Hyp  Ref  Expression 

1  f1oen.1   A e. _V 

2  f1oeng   ( ( A e. _V /\ F : A 11onto> B ) > A ~~ B ) 

3  1 2  mpan   ( F : A 11onto> B > A ~~ B ) 