Metamath Proof Explorer


Theorem fofn

Description: An onto mapping is a function on its domain. (Contributed by NM, 16-Dec-2008)

Ref Expression
Assertion fofn F : A onto B F Fn A

Proof

Step Hyp Ref Expression
1 fof F : A onto B F : A B
2 1 ffnd F : A onto B F Fn A