Theorem ffund 5486

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

Syntax hints:   -> wi 4   Fun wfun 5320   -->wf 5322

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 5329  df-f 5330

This theorem is referenced by:  swrdwrdsymbg  11249  ennnfonelemrnh  13055  ennnfonelemf1  13057  ctinfomlemom  13066  psrbaglesuppg  14705  psrelbasfun  14710  cncnp  14973  txcnp  15014  dvidlemap  15434  dvidrelem  15435  dvidsslem  15436  dvaddxx  15446  dvmulxx  15447  dvcjbr  15451  dvcj  15452  dvrecap  15456  plyaddlem1  15490  plymullem1  15491  plycoeid3  15500  uhgrfun  15947  vdegp1aid  16184  vdegp1bid  16185  wlkres  16249