Theorem ffund 5429

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

Hypothesis

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

Assertion

Ref	Expression
ffund	|- ( ph -> Fun F )

Proof of Theorem ffund

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

Syntax hints:   -> wi 4   Fun wfun 5265   -->wf 5267

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117  df-fn 5274  df-f 5275

This theorem is referenced by:  swrdwrdsymbg  11117  ennnfonelemrnh  12787  ennnfonelemf1  12789  ctinfomlemom  12798  psrbaglesuppg  14434  psrelbasfun  14439  cncnp  14702  txcnp  14743  dvidlemap  15163  dvidrelem  15164  dvidsslem  15165  dvaddxx  15175  dvmulxx  15176  dvcjbr  15180  dvcj  15181  dvrecap  15185  plyaddlem1  15219  plymullem1  15220  plycoeid3  15229