Theorem ffund 6087

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

Syntax hints:   → wi 4  Fun wfun 5920  ⟶wf 5922

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 5929  df-f 5930

This theorem is referenced by:  fofun  6154  fmptco  6436  evlslem3  19562  mdegldg  23871  uhgrfun  26006  vdegp1bi  26489  wlkreslem  26622  wlkres  26623  gneispacefun  38752  limsuppnfdlem  40251  climxrrelem  40299  climxrre  40300  liminfvalxr  40333  xlimxrre  40375  subsaliuncllem  40893  ovnovollem2  41192  preimaioomnf  41250  smfresal  41316  smfres  41318  smfco  41330