Theorem ffund 6714

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

This proof depends on syntax axioms:   → wi 4  Fun wfun 6532  ⟶wf 6534

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 6541  df-f 6542

This theorem is used by:  fofun  6797  fssrescdmd  7127  fmptco  7130  funfvima2d  7238  smores2  8365  elmapfun  8891  fidmfisupp  9367  fdmfifsupp  9370  fsuppmptif  9394  fsuppco2  9398  fsuppcor  9399  ordtypelem8  9522  ordtypelem9  9523  ordtypelem10  9524  unxpwdom2  9585  fpwwe2  10731  swrdwrdsymb  14816  mrcuni  17800  frmdss2  19064  cntzmhm2  19561  frgpupval  19993  gsumzadd  20141  gsumpt  20181  gsum2dlem2  20190  dprd2da  20263  lmhmpreima  21328  lmhmlsp  21329  rhmpreimaidl  21576  cygznlem2  21879  frlmsslsp  22107  frlmup1  22109  frlmup4  22112  lindff1  22131  lindfrn  22132  psrelbasfun  22249  mvrcl  22304  evlslem3  22394  evlseu  22397  evlsvvvallem  22405  mpfind  22429  mhpmulcl  22475  psdmul  22492  gsumply1subr  22556  cnclsi  23595  cncnp  23603  paste  23617  connima  23748  1stcfb  23768  1stccnp  23786  1stckgenlem  23877  txcnpi  23932  txcnp  23944  xkoco2cn  23982  fmfnfmlem2  24279  lmflf  24329  txflf  24330  cnextcn  24391  clssubg  24433  ghmcnp  24439  metustid  24878  metustexhalf  24880  isngp2  24921  pi1xfrval  25380  pi1coval  25386  iscfil2  25592  rrxcph  25718  ismbfd  25965  ellimc2  26202  ellimc3  26204  dvres3  26238  dvres3a  26239  dvcnv  26302  dvcnvrelem1  26342  ftc1cn  26368  mdegldg  26389  plyeq0  26535  plyaddlem1  26537  plymullem1  26538  rnplynfin  26635  plyconz  26636  ulmdv  26735  dchrelbas2  27569  dchrghm  27588  uhgrfun  29649  vdegp1ai  30122  vdegp1bi  30123  wlkres  30254  spthcycl  30397  sspg  31335  ssps  31337  sspn  31343  htthlem  31524  fmptcof2  33298  fnpreimac  33311  curry2ima  33349  offinsupp1  33364  fpwrelmapffslem  33370  indfsd  33481  swrdrn2  33563  pwrssmgc  33607  gsumhashmul  33674  xrge0tsmsd  33680  wrdpmtrlast  33700  cyc3co2  33747  tocyccntz  33751  rmfsupp2  33844  elrgspnlem1  33849  elrgspnlem2  33850  elrgspnlem3  33851  elrgspnlem4  33852  elrgspnsubrunlem1  33854  elrgspnsubrunlem2  33855  elrspunidl  34024  rhmimaidl  34028  ig1pmindeg  34180  selvascl  34195  extvfvcl  34214  mplmulmvr  34217  evlextv  34220  psrmonprod  34230  esplylem  34244  esplympl  34245  esplymhp  34246  esplyfv1  34247  ply1degltdimlem  34300  lbsdiflsp0  34304  fedgmullem1  34307  fedgmullem2  34308  evls1fldgencl  34348  fldextrspunlsp  34352  extdgfialglem1  34370  rhmpreimacnlem  34562  esumpfinvallem  34752  sibfof  35018  sitgclg  35020  eulerpartlemd  35044  eulerpartlemgu  35055  eulerpartlemgf  35057  dstrvprob  35150  dstfrvel  35152  orvclteinc  35154  cvmliftmolem1  36132  cvmliftlem3  36138  cvmliftlem10  36145  cvmliftlem13  36147  cvmlift2lem9  36162  cvmlift3lem6  36175  cvmlift3lem7  36176  satefvfmla0  36269  satefvfmla1  36276  msubrn  36380  mclsax  36420  mclsppslem  36434  mclspps  36435  weiunfr  37347  ftc1cnnc  38703  heibor1lem  38836  grpokerinj  38920  aks6d1c3  43266  aks6d1c4  43267  sticksstones1  43289  aks6d1c6lem2  43314  rhmqusspan  43328  aks5lem2  43330  imacrhmcl  43674  evlselvlem  43709  evlselv  43710  lmhmfgima  44179  cantnfub  44416  onnoxpg  44523  gneispacefun  45230  relpfrlem  46036  cncmpmax  46142  limccog  46725  limsuppnfdlem  46804  climxrrelem  46852  climxrre  46853  liminfvalxr  46886  liminflimsupxrre  46920  xlimxrre  46934  dvsinax  47016  fvvolioof  47092  fvvolicof  47094  dirkercncflem2  47207  fourierdlem82  47291  fourierdlem113  47322  subsaliuncllem  47460  fge0iccico  47473  sge0sn  47482  sge0tsms  47483  sge0cl  47484  sge0f1o  47485  sge0isum  47530  ovnovollem1  47759  ovnovollem2  47760  preimaioomnf  47822  smfresal  47891  smfres  47893  smfco  47905  tmachlem-agreesn  48050  fcoreslem1  48226  fcoreslem2  48227  fcores  48230  gricushgr  49108  ushggricedg  49118  uspgrlimlem4  49182  ffvbr  50060  cnneiima  50124  sepfsepc  50135  imaf1co  50364