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  11450  ennnfonelemrnh  13356  ennnfonelemf1  13358  ctinfomlemom  13367  psrbaglesuppg  15106  psrelbasfun  15117  cncnp  15380  txcnp  15421  dvidlemap  15841  dvidrelem  15842  dvidsslem  15843  dvaddxx  15853  dvmulxx  15854  dvcjbr  15858  dvcj  15859  dvrecap  15863  plyaddlem1  15897  plymullem1  15898  plycoeid3  15907  uhgrfun  16416  vdegp1aid  16653  vdegp1bid  16654  wlkres  16718