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  11244  ennnfonelemrnh  13036  ennnfonelemf1  13038  ctinfomlemom  13047  psrbaglesuppg  14685  psrelbasfun  14690  cncnp  14953  txcnp  14994  dvidlemap  15414  dvidrelem  15415  dvidsslem  15416  dvaddxx  15426  dvmulxx  15427  dvcjbr  15431  dvcj  15432  dvrecap  15436  plyaddlem1  15470  plymullem1  15471  plycoeid3  15480  uhgrfun  15927  vdegp1aid  16164  vdegp1bid  16165  wlkres  16229