Theorem ffund 5540

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

This proof depends on syntax axioms:   -> wi 4   Fun wfun 5374   -->wf 5376

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-fn 5383  df-f 5384

This theorem is used by:  funisfsuppdc  7298  fdmfifsupp  7301  swrdwrdsymbg  11457  ennnfonelemrnh  13364  ennnfonelemf1  13366  ctinfomlemom  13375  cntzmhm2  14173  psrbaglesuppg  15170  psrelbasfun  15190  mvrclfi  15226  mplsubgfilemcl  15232  mplsubgfileminv  15233  cncnp  15473  txcnp  15514  dvidlemap  15934  dvidrelem  15935  dvidsslem  15936  dvaddxx  15946  dvmulxx  15947  dvcjbr  15951  dvcj  15952  dvrecap  15956  plyaddlem1  15990  plymullem1  15991  plycoeid3  16000  uhgrfun  16540  vdegp1aid  16777  vdegp1bid  16778  wlkres  16842