Theorem ffund 5480

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

Syntax hints:   -> wi 4   Fun wfun 5315   -->wf 5317

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 5324  df-f 5325

This theorem is referenced by:  swrdwrdsymbg  11217  ennnfonelemrnh  13008  ennnfonelemf1  13010  ctinfomlemom  13019  psrbaglesuppg  14657  psrelbasfun  14662  cncnp  14925  txcnp  14966  dvidlemap  15386  dvidrelem  15387  dvidsslem  15388  dvaddxx  15398  dvmulxx  15399  dvcjbr  15403  dvcj  15404  dvrecap  15408  plyaddlem1  15442  plymullem1  15443  plycoeid3  15452  uhgrfun  15898  wlkres  16149