Theorem ffund 5438

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

Syntax hints:   → wi 4  Fun wfun 5273  ⟶wf 5275

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 5282  df-f 5283

This theorem is referenced by:  swrdwrdsymbg  11135  ennnfonelemrnh  12857  ennnfonelemf1  12859  ctinfomlemom  12868  psrbaglesuppg  14504  psrelbasfun  14509  cncnp  14772  txcnp  14813  dvidlemap  15233  dvidrelem  15234  dvidsslem  15235  dvaddxx  15245  dvmulxx  15246  dvcjbr  15250  dvcj  15251  dvrecap  15255  plyaddlem1  15289  plymullem1  15290  plycoeid3  15299  uhgrfun  15743