Theorem ffund 6162

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

Syntax hints:   → wi 4  Fun wfun 5995  ⟶wf 5997

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 385  df-fn 6004  df-f 6005

This theorem is referenced by:  fofun  6229  fmptco  6511  evlslem3  19637  mdegldg  23946  uhgrfun  26081  vdegp1bi  26564  wlkreslem  26697  wlkres  26698  gneispacefun  38854  limsuppnfdlem  40353  climxrrelem  40401  climxrre  40402  liminfvalxr  40435  xlimxrre  40477  subsaliuncllem  40995  ovnovollem2  41294  preimaioomnf  41352  smfresal  41418  smfres  41420  smfco  41432