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  11212  ennnfonelemrnh  13003  ennnfonelemf1  13005  ctinfomlemom  13014  psrbaglesuppg  14652  psrelbasfun  14657  cncnp  14920  txcnp  14961  dvidlemap  15381  dvidrelem  15382  dvidsslem  15383  dvaddxx  15393  dvmulxx  15394  dvcjbr  15398  dvcj  15399  dvrecap  15403  plyaddlem1  15437  plymullem1  15438  plycoeid3  15447  uhgrfun  15893  wlkres  16123