Theorem ffund 5449

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

Syntax hints:   -> wi 4   Fun wfun 5284   -->wf 5286

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 5293  df-f 5294

This theorem is referenced by:  swrdwrdsymbg  11155  ennnfonelemrnh  12902  ennnfonelemf1  12904  ctinfomlemom  12913  psrbaglesuppg  14549  psrelbasfun  14554  cncnp  14817  txcnp  14858  dvidlemap  15278  dvidrelem  15279  dvidsslem  15280  dvaddxx  15290  dvmulxx  15291  dvcjbr  15295  dvcj  15296  dvrecap  15300  plyaddlem1  15334  plymullem1  15335  plycoeid3  15344  uhgrfun  15788