Theorem ffund 5476

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

Syntax hints:   → wi 4  Fun wfun 5311  ⟶wf 5313

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

This theorem is referenced by:  swrdwrdsymbg  11191  ennnfonelemrnh  12982  ennnfonelemf1  12984  ctinfomlemom  12993  psrbaglesuppg  14630  psrelbasfun  14635  cncnp  14898  txcnp  14939  dvidlemap  15359  dvidrelem  15360  dvidsslem  15361  dvaddxx  15371  dvmulxx  15372  dvcjbr  15376  dvcj  15377  dvrecap  15381  plyaddlem1  15415  plymullem1  15416  plycoeid3  15425  uhgrfun  15871