Theorem ffund 5486

Description: A mapping is a function, deduction version. (Contributed by Glauco Siliprandi, 3-Mar-2021.)

Hypothesis

Ref	Expression
ffund.1	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)

Assertion

Ref	Expression
ffund	⊢ (𝜑 → Fun 𝐹)

Proof of Theorem ffund

Step	Hyp	Ref	Expression
1		ffund.1	. 2 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
2		ffun 5485	. 2 ⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹)
3	1, 2	syl 14	1 ⊢ (𝜑 → Fun 𝐹)

Syntax hints:   → wi 4  Fun wfun 5320  ⟶wf 5322

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 5329  df-f 5330

This theorem is referenced by:  swrdwrdsymbg  11249  ennnfonelemrnh  13042  ennnfonelemf1  13044  ctinfomlemom  13053  psrbaglesuppg  14692  psrelbasfun  14697  cncnp  14960  txcnp  15001  dvidlemap  15421  dvidrelem  15422  dvidsslem  15423  dvaddxx  15433  dvmulxx  15434  dvcjbr  15438  dvcj  15439  dvrecap  15443  plyaddlem1  15477  plymullem1  15478  plycoeid3  15487  uhgrfun  15934  vdegp1aid  16171  vdegp1bid  16172  wlkres  16236