Theorem ffund 5517

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

Syntax hints:   -> wi 4   Fun wfun 5351   -->wf 5353

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 5360  df-f 5361

This theorem is referenced by:  swrdwrdsymbg  11381  ennnfonelemrnh  13251  ennnfonelemf1  13253  ctinfomlemom  13262  psrbaglesuppg  14947  psrelbasfun  14958  cncnp  15221  txcnp  15262  dvidlemap  15682  dvidrelem  15683  dvidsslem  15684  dvaddxx  15694  dvmulxx  15695  dvcjbr  15699  dvcj  15700  dvrecap  15704  plyaddlem1  15738  plymullem1  15739  plycoeid3  15748  uhgrfun  16198  vdegp1aid  16435  vdegp1bid  16436  wlkres  16500