Theorem ffund 6260

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

Syntax hints:   → wi 4  Fun wfun 6095  ⟶wf 6097

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 199  df-an 386  df-fn 6104  df-f 6105

This theorem is referenced by:  fofun  6332  fmptco  6623  smores2  7690  elmapfun  8119  fdmfifsupp  8527  fsuppmptif  8547  fsuppco2  8550  fsuppcor  8551  ordtypelem8  8672  ordtypelem9  8673  ordtypelem10  8674  unxpwdom2  8735  fpwwe2  9753  swrdwrdsymb  13700  mrcuni  16596  cntzmhm2  18084  frgpupval  18502  gsumzadd  18637  gsumpt  18676  gsum2dlem2  18685  dprd2da  18757  lmhmpreima  19369  lmhmlsp  19370  psrelbasfun  19703  mvrcl  19772  evlslem3  19836  evlseu  19838  mpfind  19858  gsumply1subr  19926  cygznlem2  20238  frlmup1  20462  frlmup4  20465  lindff1  20484  lindfrn  20485  cnclsi  21405  cncnp  21413  paste  21427  connima  21557  1stcfb  21577  1stccnp  21594  1stckgenlem  21685  txcnpi  21740  txcnp  21752  xkoco2cn  21790  fmfnfmlem2  22087  lmflf  22137  txflf  22138  cnextcn  22199  clssubg  22240  ghmcnp  22246  metustid  22687  metustexhalf  22689  isngp2  22729  pi1xfrval  23181  pi1coval  23187  iscfil2  23392  rrxcph  23518  ismbfd  23747  ellimc2  23982  ellimc3  23984  dvres3  24018  dvres3a  24019  dvcnv  24081  dvcnvrelem1  24121  ftc1cn  24147  mdegldg  24167  plyeq0  24308  plyaddlem1  24310  plymullem1  24311  ulmdv  24498  dchrelbas2  25314  dchrghm  25333  uhgrfun  26301  vdegp1ai  26786  vdegp1bi  26787  wlkres  26921  wlkreslemOLD  26922  wlkresOLD  26923  sspg  28108  ssps  28110  sspn  28116  htthlem  28299  fmptcof2  29976  curry2ima  30004  fpwrelmapffslem  30025  xrge0tsmsd  30301  esumpfinvallem  30652  sibfof  30918  sitgclg  30920  eulerpartlemd  30944  eulerpartlemgu  30955  eulerpartlemgf  30957  dstrvprob  31050  dstfrvel  31052  orvclteinc  31054  cvmliftmolem1  31780  cvmliftlem3  31786  cvmliftlem10  31793  cvmliftlem13  31795  cvmlift2lem9  31810  cvmlift3lem6  31823  cvmlift3lem7  31824  msubrn  31943  mclsax  31983  mclsppslem  31997  mclspps  31998  ftc1cnnc  33972  heibor1lem  34095  grpokerinj  34179  lmhmfgima  38439  gneispacefun  39217  funfvima2d  39251  cncmpmax  39951  fidmfisupp  40143  limccog  40596  limsuppnfdlem  40677  climxrrelem  40725  climxrre  40726  liminfvalxr  40759  xlimxrre  40801  dvsinax  40871  fvvolioof  40949  fvvolicof  40951  dirkercncflem2  41064  fourierdlem82  41148  subsaliuncllem  41318  fge0iccico  41330  sge0sn  41339  sge0tsms  41340  sge0cl  41341  sge0f1o  41342  sge0isum  41387  ovnovollem1  41616  ovnovollem2  41617  preimaioomnf  41675  smfresal  41741  smfres  41743  smfco  41755  isomushgr  42496  ushrisomgr  42511