Metamath Proof Explorer


Theorem fofun

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

Ref Expression
Assertion fofun ( 𝐹 : 𝐴onto𝐵 → Fun 𝐹 )

Proof

Step Hyp Ref Expression
1 fof ( 𝐹 : 𝐴onto𝐵𝐹 : 𝐴𝐵 )
2 1 ffund ( 𝐹 : 𝐴onto𝐵 → Fun 𝐹 )