Theorem ffund 5414

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

Syntax hints:   → wi 4  Fun wfun 5253  ⟶wf 5255

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 5262  df-f 5263

This theorem is referenced by:  ennnfonelemrnh  12658  ennnfonelemf1  12660  ctinfomlemom  12669  psrbaglesuppg  14302  psrelbasfun  14305  cncnp  14550  txcnp  14591  dvidlemap  15011  dvidrelem  15012  dvidsslem  15013  dvaddxx  15023  dvmulxx  15024  dvcjbr  15028  dvcj  15029  dvrecap  15033  plyaddlem1  15067  plymullem1  15068  plycoeid3  15077