Theorem ffund 5537

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

This proof depends on syntax axioms:   → wi 4  Fun wfun 5371  ⟶wf 5373

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 5380  df-f 5381

This theorem is used by:  swrdwrdsymbg  11436  ennnfonelemrnh  13307  ennnfonelemf1  13309  ctinfomlemom  13318  psrbaglesuppg  15057  psrelbasfun  15068  cncnp  15331  txcnp  15372  dvidlemap  15792  dvidrelem  15793  dvidsslem  15794  dvaddxx  15804  dvmulxx  15805  dvcjbr  15809  dvcj  15810  dvrecap  15814  plyaddlem1  15848  plymullem1  15849  plycoeid3  15858  uhgrfun  16318  vdegp1aid  16555  vdegp1bid  16556  wlkres  16620