Metamath Proof Explorer


Theorem fofun

Description: An onto mapping is a function. (Contributed by NM, 29-Mar-2008)

Ref Expression
Assertion fofun
|- ( F : A -onto-> B -> Fun F )

Proof

Step Hyp Ref Expression
1 fof
 |-  ( F : A -onto-> B -> F : A --> B )
2 1 ffund
 |-  ( F : A -onto-> B -> Fun F )