Metamath Proof Explorer

Theorem ffund

Description: A mapping is a function, deduction version. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypothesis ffund.1 
|- ( ph -> F : A --> B )
Assertion ffund 
|- ( ph -> Fun F )

Proof

Step Hyp Ref Expression
1 ffund.1 
 |-  ( ph -> F : A --> B )
2 ffun 
 |-  ( F : A --> B -> Fun F )
3 1 2 syl 
 |-  ( ph -> Fun F )