Theorem ffund 5485

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

Syntax hints:   → wi 4  Fun wfun 5319  ⟶wf 5321

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

This theorem is referenced by:  swrdwrdsymbg  11251  ennnfonelemrnh  13057  ennnfonelemf1  13059  ctinfomlemom  13068  psrbaglesuppg  14707  psrelbasfun  14717  cncnp  14980  txcnp  15021  dvidlemap  15441  dvidrelem  15442  dvidsslem  15443  dvaddxx  15453  dvmulxx  15454  dvcjbr  15458  dvcj  15459  dvrecap  15463  plyaddlem1  15497  plymullem1  15498  plycoeid3  15507  uhgrfun  15954  vdegp1aid  16191  vdegp1bid  16192  wlkres  16256