Theorem ffund 6700

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

Syntax hints:   → wi 4  Fun wfun 6519  ⟶wf 6521

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 6528  df-f 6529

This theorem is referenced by:  fofun  6783  fssrescdmd  7112  fmptco  7115  funfvima2d  7220  smores2  8329  elmapfun  8851  fidmfisupp  9320  fdmfifsupp  9323  fsuppmptif  9347  fsuppco2  9351  fsuppcor  9352  ordtypelem8  9475  ordtypelem9  9476  ordtypelem10  9477  unxpwdom2  9538  fpwwe2  10616  swrdwrdsymb  14690  mrcuni  17667  frmdss2  18912  cntzmhm2  19403  frgpupval  19835  gsumzadd  19983  gsumpt  20023  gsum2dlem2  20032  dprd2da  20105  lmhmpreima  21138  lmhmlsp  21139  rhmpreimaidl  21378  cygznlem2  21678  frlmsslsp  21906  frlmup1  21908  frlmup4  21911  lindff1  21930  lindfrn  21931  psrelbasfun  22046  mvrcl  22101  evlslem3  22191  evlseu  22194  evlsvvvallem  22202  mpfind  22226  mhpmulcl  22272  psdmul  22289  gsumply1subr  22353  cnclsi  23390  cncnp  23398  paste  23412  connima  23543  1stcfb  23563  1stccnp  23580  1stckgenlem  23671  txcnpi  23726  txcnp  23738  xkoco2cn  23776  fmfnfmlem2  24073  lmflf  24123  txflf  24124  cnextcn  24185  clssubg  24227  ghmcnp  24233  metustid  24672  metustexhalf  24674  isngp2  24715  pi1xfrval  25174  pi1coval  25180  iscfil2  25386  rrxcph  25512  ismbfd  25759  ellimc2  25997  ellimc3  25999  dvres3  26033  dvres3a  26034  dvcnv  26097  dvcnvrelem1  26137  ftc1cn  26163  mdegldg  26184  plyeq0  26329  plyaddlem1  26331  plymullem1  26332  ulmdv  26524  dchrelbas2  27359  dchrghm  27378  uhgrfun  29325  vdegp1ai  29795  vdegp1bi  29796  wlkres  29927  sspg  30989  ssps  30991  sspn  30997  htthlem  31178  fmptcof2  32914  fnpreimac  32927  curry2ima  32966  offinsupp1  32983  fpwrelmapffslem  32989  indfsd  33101  swrdrn2  33187  pwrssmgc  33233  gsumhashmul  33300  xrge0tsmsd  33306  wrdpmtrlast  33326  cyc3co2  33373  tocyccntz  33377  rmfsupp2  33470  elrgspnlem1  33475  elrgspnlem2  33476  elrgspnlem3  33477  elrgspnlem4  33478  elrgspnsubrunlem1  33480  elrgspnsubrunlem2  33481  elrspunidl  33652  rhmimaidl  33656  ig1pmindeg  33809  selvascl  33824  extvfvcl  33843  mplmulmvr  33846  evlextv  33849  psrmonprod  33859  esplylem  33873  esplympl  33874  esplymhp  33875  esplyfv1  33876  ply1degltdimlem  33929  lbsdiflsp0  33933  fedgmullem1  33936  fedgmullem2  33937  evls1fldgencl  33977  fldextrspunlsp  33981  extdgfialglem1  33999  rhmpreimacnlem  34191  esumpfinvallem  34381  sibfof  34647  sitgclg  34649  eulerpartlemd  34673  eulerpartlemgu  34684  eulerpartlemgf  34686  dstrvprob  34779  dstfrvel  34781  orvclteinc  34783  spthcycl  35492  cvmliftmolem1  35644  cvmliftlem3  35650  cvmliftlem10  35657  cvmliftlem13  35659  cvmlift2lem9  35674  cvmlift3lem6  35687  cvmlift3lem7  35688  satefvfmla0  35781  satefvfmla1  35788  msubrn  35892  mclsax  35932  mclsppslem  35946  mclspps  35947  weiunfr  36840  ftc1cnnc  38203  heibor1lem  38320  grpokerinj  38404  aks6d1c3  42752  aks6d1c4  42753  sticksstones1  42775  aks6d1c6lem2  42800  rhmqusspan  42814  aks5lem2  42816  imacrhmcl  43148  evlselvlem  43182  evlselv  43183  lmhmfgima  43673  cantnfub  43910  onnoxpg  44017  gneispacefun  44725  relpfrlem  45527  cncmpmax  45610  limccog  46194  limsuppnfdlem  46273  climxrrelem  46321  climxrre  46322  liminfvalxr  46355  liminflimsupxrre  46389  xlimxrre  46403  dvsinax  46485  fvvolioof  46561  fvvolicof  46563  dirkercncflem2  46676  fourierdlem82  46760  fourierdlem113  46791  subsaliuncllem  46929  fge0iccico  46942  sge0sn  46951  sge0tsms  46952  sge0cl  46953  sge0f1o  46954  sge0isum  46999  ovnovollem1  47228  ovnovollem2  47229  preimaioomnf  47291  smfresal  47360  smfres  47362  smfco  47374  fcoreslem1  47655  fcoreslem2  47656  fcores  47659  gricushgr  48537  ushggricedg  48547  uspgrlimlem4  48611  ffvbr  49485  cnneiima  49546  sepfsepc  49557  imaf1co  49784