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  7064  fmptco  7067  funfvima2d  7172  smores2  8284  elmapfun  8800  fidmfisupp  9281  fdmfifsupp  9284  fsuppmptif  9308  fsuppco2  9312  fsuppcor  9313  ordtypelem8  9436  ordtypelem9  9437  ordtypelem10  9438  unxpwdom2  9499  fpwwe2  10556  swrdwrdsymb  14587  mrcuni  17545  frmdss2  18755  cntzmhm2  19239  frgpupval  19671  gsumzadd  19819  gsumpt  19859  gsum2dlem2  19868  dprd2da  19941  lmhmpreima  20970  lmhmlsp  20971  rhmpreimaidl  21202  cygznlem2  21493  frlmsslsp  21721  frlmup1  21723  frlmup4  21726  lindff1  21745  lindfrn  21746  psrelbasfun  21860  mvrcl  21917  evlslem3  22003  evlseu  22006  mpfind  22030  mhpmulcl  22052  psdmul  22069  gsumply1subr  22134  cnclsi  23175  cncnp  23183  paste  23197  connima  23328  1stcfb  23348  1stccnp  23365  1stckgenlem  23456  txcnpi  23511  txcnp  23523  xkoco2cn  23561  fmfnfmlem2  23858  lmflf  23908  txflf  23909  cnextcn  23970  clssubg  24012  ghmcnp  24018  metustid  24458  metustexhalf  24460  isngp2  24501  pi1xfrval  24970  pi1coval  24976  iscfil2  25182  rrxcph  25308  ismbfd  25556  ellimc2  25794  ellimc3  25796  dvres3  25830  dvres3a  25831  dvcnv  25897  dvcnvrelem1  25938  ftc1cn  25966  mdegldg  25987  plyeq0  26132  plyaddlem1  26134  plymullem1  26135  ulmdv  26328  dchrelbas2  27164  dchrghm  27183  uhgrfun  29029  vdegp1ai  29500  vdegp1bi  29501  wlkres  29632  sspg  30690  ssps  30692  sspn  30698  htthlem  30879  fmptcof2  32614  fnpreimac  32628  curry2ima  32665  offinsupp1  32683  fpwrelmapffslem  32688  swrdrn2  32909  pwrssmgc  32955  gsumhashmul  33027  xrge0tsmsd  33028  wrdpmtrlast  33048  cyc3co2  33095  tocyccntz  33099  rmfsupp2  33191  elrgspnlem1  33195  elrgspnlem2  33196  elrgspnlem3  33197  elrgspnlem4  33198  elrgspnsubrunlem1  33200  elrgspnsubrunlem2  33201  elrspunidl  33378  rhmimaidl  33382  ig1pmindeg  33546  ply1degltdimlem  33597  lbsdiflsp0  33601  fedgmullem1  33604  fedgmullem2  33605  evls1fldgencl  33644  fldextrspunlsp  33648  rhmpreimacnlem  33853  esumpfinvallem  34043  sibfof  34310  sitgclg  34312  eulerpartlemd  34336  eulerpartlemgu  34347  eulerpartlemgf  34349  dstrvprob  34442  dstfrvel  34444  orvclteinc  34446  spthcycl  35104  cvmliftmolem1  35256  cvmliftlem3  35262  cvmliftlem10  35269  cvmliftlem13  35271  cvmlift2lem9  35286  cvmlift3lem6  35299  cvmlift3lem7  35300  satefvfmla0  35393  satefvfmla1  35400  msubrn  35504  mclsax  35544  mclsppslem  35558  mclspps  35559  weiunfr  36443  ftc1cnnc  37674  heibor1lem  37791  grpokerinj  37875  aks6d1c3  42099  aks6d1c4  42100  sticksstones1  42122  aks6d1c6lem2  42147  rhmqusspan  42161  aks5lem2  42163  imacrhmcl  42490  evlsvvvallem  42537  evlselvlem  42562  evlselv  42563  lmhmfgima  43060  cantnfub  43297  onnog  43405  gneispacefun  44113  relpfrlem  44930  cncmpmax  45013  limccog  45605  limsuppnfdlem  45686  climxrrelem  45734  climxrre  45735  liminfvalxr  45768  liminflimsupxrre  45802  xlimxrre  45816  dvsinax  45898  fvvolioof  45974  fvvolicof  45976  dirkercncflem2  46089  fourierdlem82  46173  subsaliuncllem  46342  fge0iccico  46355  sge0sn  46364  sge0tsms  46365  sge0cl  46366  sge0f1o  46367  sge0isum  46412  ovnovollem1  46641  ovnovollem2  46642  preimaioomnf  46704  smfresal  46773  smfres  46775  smfco  46787  fcoreslem1  47051  fcoreslem2  47052  fcores  47055  gricushgr  47905  ushggricedg  47915  uspgrlimlem4  47979  ffvbr  48844  cnneiima  48905  sepfsepc  48916  imaf1co  49144