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 AV
Assertion f1oen F:A1-1 ontoBAB

Proof

Step Hyp Ref Expression
1 f1oen.1 AV
2 f1oeng AVF:A1-1 ontoBAB
3 1 2 mpan F:A1-1 ontoBAB