Theorem ffund 5477

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

Syntax hints:   -> wi 4   Fun wfun 5312   -->wf 5314

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 5321  df-f 5322

This theorem is referenced by:  swrdwrdsymbg  11196  ennnfonelemrnh  12987  ennnfonelemf1  12989  ctinfomlemom  12998  psrbaglesuppg  14636  psrelbasfun  14641  cncnp  14904  txcnp  14945  dvidlemap  15365  dvidrelem  15366  dvidsslem  15367  dvaddxx  15377  dvmulxx  15378  dvcjbr  15382  dvcj  15383  dvrecap  15387  plyaddlem1  15421  plymullem1  15422  plycoeid3  15431  uhgrfun  15877