Theorem ffund 5411

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

Syntax hints:   -> wi 4   Fun wfun 5252   -->wf 5254

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 5261  df-f 5262

This theorem is referenced by:  ennnfonelemrnh  12633  ennnfonelemf1  12635  ctinfomlemom  12644  psrbaglesuppg  14226  psrelbasfun  14229  cncnp  14466  txcnp  14507  dvidlemap  14927  dvidrelem  14928  dvidsslem  14929  dvaddxx  14939  dvmulxx  14940  dvcjbr  14944  dvcj  14945  dvrecap  14949  plyaddlem1  14983  plymullem1  14984  plycoeid3  14993