Theorem ffund 5477

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

Syntax hints:   → wi 4  Fun wfun 5312  ⟶wf 5314

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 5321  df-f 5322

This theorem is referenced by:  swrdwrdsymbg  11211  ennnfonelemrnh  13002  ennnfonelemf1  13004  ctinfomlemom  13013  psrbaglesuppg  14651  psrelbasfun  14656  cncnp  14919  txcnp  14960  dvidlemap  15380  dvidrelem  15381  dvidsslem  15382  dvaddxx  15392  dvmulxx  15393  dvcjbr  15397  dvcj  15398  dvrecap  15402  plyaddlem1  15436  plymullem1  15437  plycoeid3  15446  uhgrfun  15892  wlkres  16118