Theorem ffund 6692

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

Syntax hints:   → wi 4  Fun wfun 6511  ⟶wf 6513

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 209  df-an 400  df-fn 6520  df-f 6521

This theorem is referenced by:  fofun  6775  fssrescdmd  7104  fmptco  7107  funfvima2d  7212  smores2  8320  elmapfun  8843  fidmfisupp  9315  fdmfifsupp  9318  fsuppmptif  9342  fsuppco2  9346  fsuppcor  9347  ordtypelem8  9470  ordtypelem9  9471  ordtypelem10  9472  unxpwdom2  9533  fpwwe2  10598  swrdwrdsymb  14673  mrcuni  17636  frmdss2  18880  cntzmhm2  19365  frgpupval  19797  gsumzadd  19945  gsumpt  19985  gsum2dlem2  19994  dprd2da  20067  lmhmpreima  21095  lmhmlsp  21096  rhmpreimaidl  21327  cygznlem2  21600  frlmsslsp  21828  frlmup1  21830  frlmup4  21833  lindff1  21852  lindfrn  21853  psrelbasfun  21968  mvrcl  22023  evlslem3  22113  evlseu  22116  evlsvvvallem  22124  mpfind  22148  mhpmulcl  22194  psdmul  22211  gsumply1subr  22275  cnclsi  23312  cncnp  23320  paste  23334  connima  23465  1stcfb  23485  1stccnp  23502  1stckgenlem  23593  txcnpi  23648  txcnp  23660  xkoco2cn  23698  fmfnfmlem2  23995  lmflf  24045  txflf  24046  cnextcn  24107  clssubg  24149  ghmcnp  24155  metustid  24594  metustexhalf  24596  isngp2  24637  pi1xfrval  25096  pi1coval  25102  iscfil2  25308  rrxcph  25434  ismbfd  25681  ellimc2  25919  ellimc3  25921  dvres3  25955  dvres3a  25956  dvcnv  26019  dvcnvrelem1  26059  ftc1cn  26085  mdegldg  26106  plyeq0  26251  plyaddlem1  26253  plymullem1  26254  ulmdv  26443  dchrelbas2  27278  dchrghm  27297  uhgrfun  29213  vdegp1ai  29683  vdegp1bi  29684  wlkres  29815  sspg  30877  ssps  30879  sspn  30885  htthlem  31066  fmptcof2  32809  fnpreimac  32822  curry2ima  32861  offinsupp1  32878  fpwrelmapffslem  32884  indfsd  33007  swrdrn2  33093  pwrssmgc  33139  gsumhashmul  33208  xrge0tsmsd  33214  wrdpmtrlast  33234  cyc3co2  33281  tocyccntz  33285  rmfsupp2  33379  elrgspnlem1  33384  elrgspnlem2  33385  elrgspnlem3  33386  elrgspnlem4  33387  elrgspnsubrunlem1  33389  elrgspnsubrunlem2  33390  elrspunidl  33575  rhmimaidl  33579  ig1pmindeg  33759  selvascl  33775  extvfvcl  33794  mplmulmvr  33797  evlextv  33800  psrmonprod  33810  esplylem  33824  esplympl  33825  esplymhp  33826  esplyfv1  33827  ply1degltdimlem  33880  lbsdiflsp0  33884  fedgmullem1  33887  fedgmullem2  33888  evls1fldgencl  33928  fldextrspunlsp  33932  extdgfialglem1  33950  rhmpreimacnlem  34142  esumpfinvallem  34332  sibfof  34598  sitgclg  34600  eulerpartlemd  34624  eulerpartlemgu  34635  eulerpartlemgf  34637  dstrvprob  34730  dstfrvel  34732  orvclteinc  34734  spthcycl  35443  cvmliftmolem1  35595  cvmliftlem3  35601  cvmliftlem10  35608  cvmliftlem13  35610  cvmlift2lem9  35625  cvmlift3lem6  35638  cvmlift3lem7  35639  satefvfmla0  35732  satefvfmla1  35739  msubrn  35843  mclsax  35883  mclsppslem  35897  mclspps  35898  weiunfr  36791  ftc1cnnc  38155  heibor1lem  38272  grpokerinj  38356  aks6d1c3  42704  aks6d1c4  42705  sticksstones1  42727  aks6d1c6lem2  42752  rhmqusspan  42766  aks5lem2  42768  imacrhmcl  43100  evlselvlem  43134  evlselv  43135  lmhmfgima  43625  cantnfub  43862  onnoxpg  43969  gneispacefun  44677  relpfrlem  45493  cncmpmax  45576  limccog  46160  limsuppnfdlem  46239  climxrrelem  46287  climxrre  46288  liminfvalxr  46321  liminflimsupxrre  46355  xlimxrre  46369  dvsinax  46451  fvvolioof  46527  fvvolicof  46529  dirkercncflem2  46642  fourierdlem82  46726  fourierdlem113  46757  subsaliuncllem  46895  fge0iccico  46908  sge0sn  46917  sge0tsms  46918  sge0cl  46919  sge0f1o  46920  sge0isum  46965  ovnovollem1  47194  ovnovollem2  47195  preimaioomnf  47257  smfresal  47326  smfres  47328  smfco  47340  fcoreslem1  47621  fcoreslem2  47622  fcores  47625  gricushgr  48503  ushggricedg  48513  uspgrlimlem4  48577  ffvbr  49441  cnneiima  49502  sepfsepc  49513  imaf1co  49740