Theorem ffund 6672

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

Syntax hints:   → wi 4  Fun wfun 6492  ⟶wf 6494

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 6501  df-f 6502

This theorem is referenced by:  fofun  6753  fssrescdmd  7079  fmptco  7082  funfvima2d  7187  smores2  8294  elmapfun  8813  fidmfisupp  9285  fdmfifsupp  9288  fsuppmptif  9312  fsuppco2  9316  fsuppcor  9317  ordtypelem8  9440  ordtypelem9  9441  ordtypelem10  9442  unxpwdom2  9503  fpwwe2  10566  swrdwrdsymb  14625  mrcuni  17587  frmdss2  18831  cntzmhm2  19317  frgpupval  19749  gsumzadd  19897  gsumpt  19937  gsum2dlem2  19946  dprd2da  20019  lmhmpreima  21043  lmhmlsp  21044  rhmpreimaidl  21275  cygznlem2  21548  frlmsslsp  21776  frlmup1  21778  frlmup4  21781  lindff1  21800  lindfrn  21801  psrelbasfun  21915  mvrcl  21970  evlslem3  22058  evlseu  22061  evlsvvvallem  22069  mpfind  22093  mhpmulcl  22115  psdmul  22132  gsumply1subr  22197  cnclsi  23237  cncnp  23245  paste  23259  connima  23390  1stcfb  23410  1stccnp  23427  1stckgenlem  23518  txcnpi  23573  txcnp  23585  xkoco2cn  23623  fmfnfmlem2  23920  lmflf  23970  txflf  23971  cnextcn  24032  clssubg  24074  ghmcnp  24080  metustid  24519  metustexhalf  24521  isngp2  24562  pi1xfrval  25021  pi1coval  25027  iscfil2  25233  rrxcph  25359  ismbfd  25606  ellimc2  25844  ellimc3  25846  dvres3  25880  dvres3a  25881  dvcnv  25944  dvcnvrelem1  25984  ftc1cn  26010  mdegldg  26031  plyeq0  26176  plyaddlem1  26178  plymullem1  26179  ulmdv  26368  dchrelbas2  27200  dchrghm  27219  uhgrfun  29135  vdegp1ai  29605  vdegp1bi  29606  wlkres  29737  sspg  30799  ssps  30801  sspn  30807  htthlem  30988  fmptcof2  32730  fnpreimac  32743  curry2ima  32782  offinsupp1  32799  fpwrelmapffslem  32805  indfsd  32928  swrdrn2  33014  pwrssmgc  33060  gsumhashmul  33128  xrge0tsmsd  33134  wrdpmtrlast  33154  cyc3co2  33201  tocyccntz  33205  rmfsupp2  33299  elrgspnlem1  33303  elrgspnlem2  33304  elrgspnlem3  33305  elrgspnlem4  33306  elrgspnsubrunlem1  33308  elrgspnsubrunlem2  33309  elrspunidl  33488  rhmimaidl  33492  ig1pmindeg  33662  extvfvcl  33680  mplmulmvr  33683  evlextv  33686  psrmonprod  33696  esplylem  33710  esplympl  33711  esplymhp  33712  esplyfv1  33713  ply1degltdimlem  33766  lbsdiflsp0  33770  fedgmullem1  33773  fedgmullem2  33774  evls1fldgencl  33814  fldextrspunlsp  33818  extdgfialglem1  33836  rhmpreimacnlem  34028  esumpfinvallem  34218  sibfof  34484  sitgclg  34486  eulerpartlemd  34510  eulerpartlemgu  34521  eulerpartlemgf  34523  dstrvprob  34616  dstfrvel  34618  orvclteinc  34620  spthcycl  35311  cvmliftmolem1  35463  cvmliftlem3  35469  cvmliftlem10  35476  cvmliftlem13  35478  cvmlift2lem9  35493  cvmlift3lem6  35506  cvmlift3lem7  35507  satefvfmla0  35600  satefvfmla1  35607  msubrn  35711  mclsax  35751  mclsppslem  35765  mclspps  35766  weiunfr  36649  ftc1cnnc  38013  heibor1lem  38130  grpokerinj  38214  aks6d1c3  42562  aks6d1c4  42563  sticksstones1  42585  aks6d1c6lem2  42610  rhmqusspan  42624  aks5lem2  42626  imacrhmcl  42959  evlselvlem  43019  evlselv  43020  lmhmfgima  43512  cantnfub  43749  onnoxpg  43856  gneispacefun  44564  relpfrlem  45380  cncmpmax  45463  limccog  46050  limsuppnfdlem  46129  climxrrelem  46177  climxrre  46178  liminfvalxr  46211  liminflimsupxrre  46245  xlimxrre  46259  dvsinax  46341  fvvolioof  46417  fvvolicof  46419  dirkercncflem2  46532  fourierdlem82  46616  subsaliuncllem  46785  fge0iccico  46798  sge0sn  46807  sge0tsms  46808  sge0cl  46809  sge0f1o  46810  sge0isum  46855  ovnovollem1  47084  ovnovollem2  47085  preimaioomnf  47147  smfresal  47216  smfres  47218  smfco  47230  fcoreslem1  47511  fcoreslem2  47512  fcores  47515  gricushgr  48393  ushggricedg  48403  uspgrlimlem4  48467  ffvbr  49331  cnneiima  49392  sepfsepc  49403  imaf1co  49630