Metamath Proof Explorer


Theorem ffun

Description: A mapping is a function. (Contributed by NM, 3-Aug-1994)

Ref Expression
Assertion ffun F : A B Fun F

Proof

Step Hyp Ref Expression
1 ffn F : A B F Fn A
2 fnfun F Fn A Fun F
3 1 2 syl F : A B Fun F