Theorem ffund 6736

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

This proof depends on syntax axioms:   → wi 4  Fun wfun 6552  ⟶wf 6554

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fn 6561  df-f 6562

This theorem is used by:  fofun  6819  fssrescdmd  7151  fmptco  7154  funfvima2d  7261  smores2  8390  elmapfun  8916  fdmfifsupp  9394  fsuppmptif  9418  fsuppco2  9422  fsuppcor  9423  ordtypelem8  9546  ordtypelem9  9547  ordtypelem10  9548  unxpwdom2  9609  fpwwe2  10755  swrdwrdsymb  14840  mrcuni  17824  frmdss2  19088  cntzmhm2  19586  frgpupval  20018  gsumzadd  20166  gsumpt  20206  gsum2dlem2  20215  dprd2da  20288  lmhmpreima  21353  lmhmlsp  21354  rhmpreimaidl  21601  cygznlem2  21904  frlmsslsp  22132  frlmup1  22134  frlmup4  22137  lindff1  22156  lindfrn  22157  psrelbasfun  22274  mvrcl  22329  evlslem3  22419  evlseu  22422  evlsvvvallem  22430  mpfind  22454  mhpmulcl  22500  psdmul  22517  gsumply1subr  22581  cnclsi  23620  cncnp  23628  paste  23642  connima  23773  1stcfb  23793  1stccnp  23811  1stckgenlem  23902  txcnpi  23957  txcnp  23969  xkoco2cn  24007  fmfnfmlem2  24304  lmflf  24354  txflf  24355  cnextcn  24416  clssubg  24458  ghmcnp  24464  metustid  24903  metustexhalf  24905  isngp2  24946  pi1xfrval  25405  pi1coval  25411  iscfil2  25617  rrxcph  25743  ismbfd  25990  ellimc2  26227  ellimc3  26229  dvres3  26263  dvres3a  26264  dvcnv  26327  dvcnvrelem1  26367  ftc1cn  26393  mdegldg  26414  plyeq0  26560  plyaddlem1  26562  plymullem1  26563  rnplynfin  26660  plyconz  26661  ulmdv  26760  dchrelbas2  27594  dchrghm  27613  uhgrfun  29674  vdegp1ai  30147  vdegp1bi  30148  wlkres  30279  spthcycl  30422  sspg  31360  ssps  31362  sspn  31368  htthlem  31549  fmptcof2  33323  fnpreimac  33336  curry2ima  33373  offinsupp1  33388  fpwrelmapffslem  33394  indfsd  33505  swrdrn2  33587  pwrssmgc  33631  gsumhashmul  33698  xrge0tsmsd  33704  wrdpmtrlast  33724  cyc3co2  33771  tocyccntz  33775  rmfsupp2  33868  elrgspnlem1  33873  elrgspnlem2  33874  elrgspnlem3  33875  elrgspnlem4  33876  elrgspnsubrunlem1  33878  elrgspnsubrunlem2  33879  elrspunidl  34048  rhmimaidl  34052  ig1pmindeg  34204  selvascl  34219  extvfvcl  34238  mplmulmvr  34241  evlextv  34244  psrmonprod  34254  esplylem  34268  esplympl  34269  esplymhp  34270  esplyfv1  34271  ply1degltdimlem  34324  lbsdiflsp0  34328  fedgmullem1  34331  fedgmullem2  34332  evls1fldgencl  34372  fldextrspunlsp  34376  extdgfialglem1  34394  rhmpreimacnlem  34586  esumpfinvallem  34776  sibfof  35042  sitgclg  35044  eulerpartlemd  35068  eulerpartlemgu  35079  eulerpartlemgf  35081  dstrvprob  35174  dstfrvel  35176  orvclteinc  35178  cvmliftmolem1  36213  cvmliftlem3  36219  cvmliftlem10  36226  cvmliftlem13  36228  cvmlift2lem9  36243  cvmlift3lem6  36256  cvmlift3lem7  36257  satefvfmla0  36350  satefvfmla1  36357  msubrn  36461  mclsax  36501  mclsppslem  36515  mclspps  36516  weiunfr  37433  ftc1cnnc  38802  heibor1lem  38935  grpokerinj  39019  aks6d1c3  43365  aks6d1c4  43366  sticksstones1  43388  aks6d1c6lem2  43413  rhmqusspan  43427  aks5lem2  43429  imacrhmcl  43774  evlselvlem  43809  evlselv  43810  lmhmfgima  44279  cantnfub  44515  onnoxpg  44622  gneispacefun  45329  relpfrlem  46138  cncmpmax  46254  limccog  46837  limsuppnfdlem  46916  climxrrelem  46964  climxrre  46965  liminfvalxr  46998  liminflimsupxrre  47032  xlimxrre  47046  dvsinax  47128  fvvolioof  47204  fvvolicof  47206  dirkercncflem2  47319  fourierdlem82  47403  fourierdlem113  47434  subsaliuncllem  47572  fge0iccico  47585  sge0sn  47594  sge0tsms  47595  sge0cl  47596  sge0f1o  47597  sge0isum  47642  ovnovollem1  47871  ovnovollem2  47872  preimaioomnf  47934  smfresal  48003  smfres  48005  smfco  48017  tmachlem-agreesn  48162  fcoreslem1  48338  fcoreslem2  48339  fcores  48342  gricushgr  49220  ushggricedg  49230  uspgrlimlem4  49294  ffvbr  50172  cnneiima  50236  sepfsepc  50247  imaf1co  50476