Theorem ffund 6660

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

Syntax hints:   → wi 4  Fun wfun 6480  ⟶wf 6482

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 207  df-an 396  df-fn 6489  df-f 6490

This theorem is referenced by:  fofun  6741  fssrescdmd  7065  fmptco  7068  funfvima2d  7172  smores2  8280  elmapfun  8796  fidmfisupp  9263  fdmfifsupp  9266  fsuppmptif  9290  fsuppco2  9294  fsuppcor  9295  ordtypelem8  9418  ordtypelem9  9419  ordtypelem10  9420  unxpwdom2  9481  fpwwe2  10541  swrdwrdsymb  14572  mrcuni  17529  frmdss2  18773  cntzmhm2  19256  frgpupval  19688  gsumzadd  19836  gsumpt  19876  gsum2dlem2  19885  dprd2da  19958  lmhmpreima  20984  lmhmlsp  20985  rhmpreimaidl  21216  cygznlem2  21507  frlmsslsp  21735  frlmup1  21737  frlmup4  21740  lindff1  21759  lindfrn  21760  psrelbasfun  21874  mvrcl  21930  evlslem3  22016  evlseu  22019  mpfind  22043  mhpmulcl  22065  psdmul  22082  gsumply1subr  22147  cnclsi  23188  cncnp  23196  paste  23210  connima  23341  1stcfb  23361  1stccnp  23378  1stckgenlem  23469  txcnpi  23524  txcnp  23536  xkoco2cn  23574  fmfnfmlem2  23871  lmflf  23921  txflf  23922  cnextcn  23983  clssubg  24025  ghmcnp  24031  metustid  24470  metustexhalf  24472  isngp2  24513  pi1xfrval  24982  pi1coval  24988  iscfil2  25194  rrxcph  25320  ismbfd  25568  ellimc2  25806  ellimc3  25808  dvres3  25842  dvres3a  25843  dvcnv  25909  dvcnvrelem1  25950  ftc1cn  25978  mdegldg  25999  plyeq0  26144  plyaddlem1  26146  plymullem1  26147  ulmdv  26340  dchrelbas2  27176  dchrghm  27195  uhgrfun  29046  vdegp1ai  29517  vdegp1bi  29518  wlkres  29649  sspg  30710  ssps  30712  sspn  30718  htthlem  30899  fmptcof2  32641  fnpreimac  32655  curry2ima  32694  offinsupp1  32713  fpwrelmapffslem  32719  indfsd  32856  swrdrn2  32942  pwrssmgc  32988  gsumhashmul  33048  xrge0tsmsd  33049  wrdpmtrlast  33069  cyc3co2  33116  tocyccntz  33120  rmfsupp2  33212  elrgspnlem1  33216  elrgspnlem2  33217  elrgspnlem3  33218  elrgspnlem4  33219  elrgspnsubrunlem1  33221  elrgspnsubrunlem2  33222  elrspunidl  33400  rhmimaidl  33404  ig1pmindeg  33569  extvfvcl  33587  mplmulmvr  33590  esplylem  33606  esplympl  33607  esplymhp  33608  esplyfv1  33609  ply1degltdimlem  33656  lbsdiflsp0  33660  fedgmullem1  33663  fedgmullem2  33664  evls1fldgencl  33704  fldextrspunlsp  33708  extdgfialglem1  33726  rhmpreimacnlem  33918  esumpfinvallem  34108  sibfof  34374  sitgclg  34376  eulerpartlemd  34400  eulerpartlemgu  34411  eulerpartlemgf  34413  dstrvprob  34506  dstfrvel  34508  orvclteinc  34510  spthcycl  35194  cvmliftmolem1  35346  cvmliftlem3  35352  cvmliftlem10  35359  cvmliftlem13  35361  cvmlift2lem9  35376  cvmlift3lem6  35389  cvmlift3lem7  35390  satefvfmla0  35483  satefvfmla1  35490  msubrn  35594  mclsax  35634  mclsppslem  35648  mclspps  35649  weiunfr  36532  ftc1cnnc  37753  heibor1lem  37870  grpokerinj  37954  aks6d1c3  42237  aks6d1c4  42238  sticksstones1  42260  aks6d1c6lem2  42285  rhmqusspan  42299  aks5lem2  42301  imacrhmcl  42633  evlsvvvallem  42680  evlselvlem  42705  evlselv  42706  lmhmfgima  43202  cantnfub  43439  onnog  43547  gneispacefun  44255  relpfrlem  45071  cncmpmax  45154  limccog  45745  limsuppnfdlem  45824  climxrrelem  45872  climxrre  45873  liminfvalxr  45906  liminflimsupxrre  45940  xlimxrre  45954  dvsinax  46036  fvvolioof  46112  fvvolicof  46114  dirkercncflem2  46227  fourierdlem82  46311  subsaliuncllem  46480  fge0iccico  46493  sge0sn  46502  sge0tsms  46503  sge0cl  46504  sge0f1o  46505  sge0isum  46550  ovnovollem1  46779  ovnovollem2  46780  preimaioomnf  46842  smfresal  46911  smfres  46913  smfco  46925  fcoreslem1  47188  fcoreslem2  47189  fcores  47192  gricushgr  48042  ushggricedg  48052  uspgrlimlem4  48116  ffvbr  48981  cnneiima  49042  sepfsepc  49053  imaf1co  49281