Theorem ffund 6049

Description: A mapping is a function, deduction version. (Contributed by Glauco Siliprandi, 3-Mar-2021.)

Hypothesis

Ref	Expression
ffund.1	|- ( ph -> F : A --> B )

Assertion

Ref	Expression
ffund	|- ( ph -> Fun F )

Proof of Theorem ffund

Step	Hyp	Ref	Expression
1		ffund.1	. 2 |- ( ph -> F : A --> B )
2		ffun 6048	. 2 |- ( F : A --> B -> Fun F )
3	1, 2	syl 17	1 |- ( ph -> Fun F )

Syntax hints:   -> wi 4   Fun wfun 5882   -->wf 5884

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 386  df-fn 5891  df-f 5892

This theorem is referenced by:  fofun  6116  fmptco  6396  evlslem3  19514  mdegldg  23826  uhgrfun  25961  vdegp1bi  26433  wlkreslem  26566  wlkres  26567  gneispacefun  38435  limsuppnfdlem  39933  climxrrelem  39981  climxrre  39982  liminfvalxr  40015  xlimxrre  40057  subsaliuncllem  40575  ovnovollem2  40871  preimaioomnf  40929  smfresal  40995  smfres  40997  smfco  41009