Theorem ffund 5493

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 5492	. 2 |- ( F : A --> B -> Fun F )
3	1, 2	syl 14	1 |- ( ph -> Fun F )

Syntax hints:   -> wi 4   Fun wfun 5327   -->wf 5329

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 5336  df-f 5337

This theorem is referenced by:  swrdwrdsymbg  11311  ennnfonelemrnh  13117  ennnfonelemf1  13119  ctinfomlemom  13128  psrbaglesuppg  14768  psrelbasfun  14778  cncnp  15041  txcnp  15082  dvidlemap  15502  dvidrelem  15503  dvidsslem  15504  dvaddxx  15514  dvmulxx  15515  dvcjbr  15519  dvcj  15520  dvrecap  15524  plyaddlem1  15558  plymullem1  15559  plycoeid3  15568  uhgrfun  16018  vdegp1aid  16255  vdegp1bid  16256  wlkres  16320