Theorem ffund 5532

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

Syntax hints:   -> wi 4   Fun wfun 5366   -->wf 5368

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 5375  df-f 5376

This theorem is referenced by:  swrdwrdsymbg  11414  ennnfonelemrnh  13285  ennnfonelemf1  13287  ctinfomlemom  13296  psrbaglesuppg  14980  psrelbasfun  14991  cncnp  15254  txcnp  15295  dvidlemap  15715  dvidrelem  15716  dvidsslem  15717  dvaddxx  15727  dvmulxx  15728  dvcjbr  15732  dvcj  15733  dvrecap  15737  plyaddlem1  15771  plymullem1  15772  plycoeid3  15781  uhgrfun  16232  vdegp1aid  16469  vdegp1bid  16470  wlkres  16534