Theorem ffund 6712

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

Syntax hints:   → wi 4  Fun wfun 6532  ⟶wf 6534

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 210  df-an 401  df-fn 6541  df-f 6542

This theorem is referenced by:  fofun  6795  fssrescdmd  7124  fmptco  7127  funfvima2d  7232  smores2  8342  elmapfun  8864  fidmfisupp  9333  fdmfifsupp  9336  fsuppmptif  9360  fsuppco2  9364  fsuppcor  9365  ordtypelem8  9488  ordtypelem9  9489  ordtypelem10  9490  unxpwdom2  9551  fpwwe2  10629  swrdwrdsymb  14702  mrcuni  17678  frmdss2  18923  cntzmhm2  19413  frgpupval  19845  gsumzadd  19993  gsumpt  20033  gsum2dlem2  20042  dprd2da  20115  lmhmpreima  21150  lmhmlsp  21151  rhmpreimaidl  21397  cygznlem2  21699  frlmsslsp  21927  frlmup1  21929  frlmup4  21932  lindff1  21951  lindfrn  21952  psrelbasfun  22067  mvrcl  22122  evlslem3  22212  evlseu  22215  evlsvvvallem  22223  mpfind  22247  mhpmulcl  22293  psdmul  22310  gsumply1subr  22374  cnclsi  23410  cncnp  23418  paste  23432  connima  23563  1stcfb  23583  1stccnp  23600  1stckgenlem  23691  txcnpi  23746  txcnp  23758  xkoco2cn  23796  fmfnfmlem2  24093  lmflf  24143  txflf  24144  cnextcn  24205  clssubg  24247  ghmcnp  24253  metustid  24692  metustexhalf  24694  isngp2  24735  pi1xfrval  25194  pi1coval  25200  iscfil2  25406  rrxcph  25532  ismbfd  25779  ellimc2  26017  ellimc3  26019  dvres3  26053  dvres3a  26054  dvcnv  26117  dvcnvrelem1  26157  ftc1cn  26183  mdegldg  26204  plyeq0  26349  plyaddlem1  26351  plymullem1  26352  ulmdv  26544  dchrelbas2  27379  dchrghm  27398  uhgrfun  29394  vdegp1ai  29864  vdegp1bi  29865  wlkres  29996  sspg  31058  ssps  31060  sspn  31066  htthlem  31247  fmptcof2  32980  fnpreimac  32993  curry2ima  33032  offinsupp1  33049  fpwrelmapffslem  33055  indfsd  33166  swrdrn2  33252  pwrssmgc  33298  gsumhashmul  33365  xrge0tsmsd  33371  wrdpmtrlast  33391  cyc3co2  33438  tocyccntz  33442  rmfsupp2  33535  elrgspnlem1  33540  elrgspnlem2  33541  elrgspnlem3  33542  elrgspnlem4  33543  elrgspnsubrunlem1  33545  elrgspnsubrunlem2  33546  elrspunidl  33714  rhmimaidl  33718  ig1pmindeg  33870  selvascl  33885  extvfvcl  33904  mplmulmvr  33907  evlextv  33910  psrmonprod  33920  esplylem  33934  esplympl  33935  esplymhp  33936  esplyfv1  33937  ply1degltdimlem  33990  lbsdiflsp0  33994  fedgmullem1  33997  fedgmullem2  33998  evls1fldgencl  34038  fldextrspunlsp  34042  extdgfialglem1  34060  rhmpreimacnlem  34252  esumpfinvallem  34442  sibfof  34708  sitgclg  34710  eulerpartlemd  34734  eulerpartlemgu  34745  eulerpartlemgf  34747  dstrvprob  34840  dstfrvel  34842  orvclteinc  34844  spthcycl  35599  cvmliftmolem1  35751  cvmliftlem3  35757  cvmliftlem10  35764  cvmliftlem13  35766  cvmlift2lem9  35781  cvmlift3lem6  35794  cvmlift3lem7  35795  satefvfmla0  35888  satefvfmla1  35895  msubrn  35999  mclsax  36039  mclsppslem  36053  mclspps  36054  weiunfr  36956  ftc1cnnc  38321  heibor1lem  38438  grpokerinj  38522  aks6d1c3  42868  aks6d1c4  42869  sticksstones1  42891  aks6d1c6lem2  42916  rhmqusspan  42930  aks5lem2  42932  imacrhmcl  43266  evlselvlem  43300  evlselv  43301  lmhmfgima  43791  cantnfub  44028  onnoxpg  44135  gneispacefun  44843  relpfrlem  45642  cncmpmax  45732  limccog  46316  limsuppnfdlem  46395  climxrrelem  46443  climxrre  46444  liminfvalxr  46477  liminflimsupxrre  46511  xlimxrre  46525  dvsinax  46607  fvvolioof  46683  fvvolicof  46685  dirkercncflem2  46798  fourierdlem82  46882  fourierdlem113  46913  subsaliuncllem  47051  fge0iccico  47064  sge0sn  47073  sge0tsms  47074  sge0cl  47075  sge0f1o  47076  sge0isum  47121  ovnovollem1  47350  ovnovollem2  47351  preimaioomnf  47413  smfresal  47482  smfres  47484  smfco  47496  fcoreslem1  47777  fcoreslem2  47778  fcores  47781  gricushgr  48659  ushggricedg  48669  uspgrlimlem4  48733  ffvbr  49611  cnneiima  49672  sepfsepc  49683  imaf1co  49910