Theorem ffund 6666

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

Syntax hints:   → wi 4  Fun wfun 6486  ⟶wf 6488

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 6495  df-f 6496

This theorem is referenced by:  fofun  6747  fssrescdmd  7071  fmptco  7074  funfvima2d  7178  smores2  8286  elmapfun  8803  fidmfisupp  9275  fdmfifsupp  9278  fsuppmptif  9302  fsuppco2  9306  fsuppcor  9307  ordtypelem8  9430  ordtypelem9  9431  ordtypelem10  9432  unxpwdom2  9493  fpwwe2  10554  swrdwrdsymb  14586  mrcuni  17544  frmdss2  18788  cntzmhm2  19271  frgpupval  19703  gsumzadd  19851  gsumpt  19891  gsum2dlem2  19900  dprd2da  19973  lmhmpreima  21000  lmhmlsp  21001  rhmpreimaidl  21232  cygznlem2  21523  frlmsslsp  21751  frlmup1  21753  frlmup4  21756  lindff1  21775  lindfrn  21776  psrelbasfun  21891  mvrcl  21947  evlslem3  22035  evlseu  22038  evlsvvvallem  22046  mpfind  22070  mhpmulcl  22092  psdmul  22109  gsumply1subr  22174  cnclsi  23216  cncnp  23224  paste  23238  connima  23369  1stcfb  23389  1stccnp  23406  1stckgenlem  23497  txcnpi  23552  txcnp  23564  xkoco2cn  23602  fmfnfmlem2  23899  lmflf  23949  txflf  23950  cnextcn  24011  clssubg  24053  ghmcnp  24059  metustid  24498  metustexhalf  24500  isngp2  24541  pi1xfrval  25010  pi1coval  25016  iscfil2  25222  rrxcph  25348  ismbfd  25596  ellimc2  25834  ellimc3  25836  dvres3  25870  dvres3a  25871  dvcnv  25937  dvcnvrelem1  25978  ftc1cn  26006  mdegldg  26027  plyeq0  26172  plyaddlem1  26174  plymullem1  26175  ulmdv  26368  dchrelbas2  27204  dchrghm  27223  uhgrfun  29139  vdegp1ai  29610  vdegp1bi  29611  wlkres  29742  sspg  30803  ssps  30805  sspn  30811  htthlem  30992  fmptcof2  32735  fnpreimac  32749  curry2ima  32788  offinsupp1  32805  fpwrelmapffslem  32811  indfsd  32950  swrdrn2  33036  pwrssmgc  33082  gsumhashmul  33150  xrge0tsmsd  33155  wrdpmtrlast  33175  cyc3co2  33222  tocyccntz  33226  rmfsupp2  33320  elrgspnlem1  33324  elrgspnlem2  33325  elrgspnlem3  33326  elrgspnlem4  33327  elrgspnsubrunlem1  33329  elrgspnsubrunlem2  33330  elrspunidl  33509  rhmimaidl  33513  ig1pmindeg  33683  extvfvcl  33701  mplmulmvr  33704  evlextv  33707  esplylem  33724  esplympl  33725  esplymhp  33726  esplyfv1  33727  ply1degltdimlem  33779  lbsdiflsp0  33783  fedgmullem1  33786  fedgmullem2  33787  evls1fldgencl  33827  fldextrspunlsp  33831  extdgfialglem1  33849  rhmpreimacnlem  34041  esumpfinvallem  34231  sibfof  34497  sitgclg  34499  eulerpartlemd  34523  eulerpartlemgu  34534  eulerpartlemgf  34536  dstrvprob  34629  dstfrvel  34631  orvclteinc  34633  spthcycl  35323  cvmliftmolem1  35475  cvmliftlem3  35481  cvmliftlem10  35488  cvmliftlem13  35490  cvmlift2lem9  35505  cvmlift3lem6  35518  cvmlift3lem7  35519  satefvfmla0  35612  satefvfmla1  35619  msubrn  35723  mclsax  35763  mclsppslem  35777  mclspps  35778  weiunfr  36661  ftc1cnnc  37889  heibor1lem  38006  grpokerinj  38090  aks6d1c3  42373  aks6d1c4  42374  sticksstones1  42396  aks6d1c6lem2  42421  rhmqusspan  42435  aks5lem2  42437  imacrhmcl  42765  evlselvlem  42825  evlselv  42826  lmhmfgima  43322  cantnfub  43559  onnoxpg  43666  gneispacefun  44374  relpfrlem  45190  cncmpmax  45273  limccog  45862  limsuppnfdlem  45941  climxrrelem  45989  climxrre  45990  liminfvalxr  46023  liminflimsupxrre  46057  xlimxrre  46071  dvsinax  46153  fvvolioof  46229  fvvolicof  46231  dirkercncflem2  46344  fourierdlem82  46428  subsaliuncllem  46597  fge0iccico  46610  sge0sn  46619  sge0tsms  46620  sge0cl  46621  sge0f1o  46622  sge0isum  46667  ovnovollem1  46896  ovnovollem2  46897  preimaioomnf  46959  smfresal  47028  smfres  47030  smfco  47042  fcoreslem1  47305  fcoreslem2  47306  fcores  47309  gricushgr  48159  ushggricedg  48169  uspgrlimlem4  48233  ffvbr  49097  cnneiima  49158  sepfsepc  49169  imaf1co  49396