Theorem ffund 5483

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

Syntax hints:   → wi 4  Fun wfun 5318  ⟶wf 5320

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 5327  df-f 5328

This theorem is referenced by:  swrdwrdsymbg  11235  ennnfonelemrnh  13027  ennnfonelemf1  13029  ctinfomlemom  13038  psrbaglesuppg  14676  psrelbasfun  14681  cncnp  14944  txcnp  14985  dvidlemap  15405  dvidrelem  15406  dvidsslem  15407  dvaddxx  15417  dvmulxx  15418  dvcjbr  15422  dvcj  15423  dvrecap  15427  plyaddlem1  15461  plymullem1  15462  plycoeid3  15471  uhgrfun  15918  wlkres  16174