Theorem ffund 5540

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 5539	. 2 ⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹)
3	1, 2	syl 14	1 ⊢ (𝜑 → Fun 𝐹)

This proof depends on syntax axioms:   → wi 4  Fun wfun 5374  ⟶wf 5376

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-fn 5383  df-f 5384

This theorem is used by:  swrdwrdsymbg  11458  ennnfonelemrnh  13365  ennnfonelemf1  13367  ctinfomlemom  13376  cntzmhm2  14174  psrbaglesuppg  15166  psrelbasfun  15181  cncnp  15456  txcnp  15497  dvidlemap  15917  dvidrelem  15918  dvidsslem  15919  dvaddxx  15929  dvmulxx  15930  dvcjbr  15934  dvcj  15935  dvrecap  15939  plyaddlem1  15973  plymullem1  15974  plycoeid3  15983  uhgrfun  16523  vdegp1aid  16760  vdegp1bid  16761  wlkres  16825