Description: A mapping is a function with domain, deduction form. (Contributed by Glauco Siliprandi, 17Aug2020)
Ref  Expression  

Hypothesis  ffnd.1   ( ph > F : A > B ) 

Assertion  ffnd   ( ph > F Fn A ) 
Step  Hyp  Ref  Expression 

1  ffnd.1   ( ph > F : A > B ) 

2  ffn   ( F : A > B > F Fn A ) 

3  1 2  syl   ( ph > F Fn A ) 