Theorem ffund 6520

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

Syntax hints:   → wi 4  Fun wfun 6351  ⟶wf 6353

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 209  df-an 399  df-fn 6360  df-f 6361

This theorem is referenced by:  fofun  6593  fmptco  6893  funfvima2d  6996  smores2  7993  elmapfun  8432  fdmfifsupp  8845  fsuppmptif  8865  fsuppco2  8868  fsuppcor  8869  ordtypelem8  8991  ordtypelem9  8992  ordtypelem10  8993  unxpwdom2  9054  fpwwe2  10067  swrdwrdsymb  14026  mrcuni  16894  frmdss2  18030  cntzmhm2  18472  frgpupval  18902  gsumzadd  19044  gsumpt  19084  gsum2dlem2  19093  dprd2da  19166  lmhmpreima  19822  lmhmlsp  19823  psrelbasfun  20162  mvrcl  20231  evlslem3  20295  evlseu  20298  mpfind  20322  gsumply1subr  20404  cygznlem2  20717  frlmsslsp  20942  frlmup1  20944  frlmup4  20947  lindff1  20966  lindfrn  20967  cnclsi  21882  cncnp  21890  paste  21904  connima  22035  1stcfb  22055  1stccnp  22072  1stckgenlem  22163  txcnpi  22218  txcnp  22230  xkoco2cn  22268  fmfnfmlem2  22565  lmflf  22615  txflf  22616  cnextcn  22677  clssubg  22719  ghmcnp  22725  metustid  23166  metustexhalf  23168  isngp2  23208  pi1xfrval  23660  pi1coval  23666  iscfil2  23871  rrxcph  23997  ismbfd  24242  ellimc2  24477  ellimc3  24479  dvres3  24513  dvres3a  24514  dvcnv  24576  dvcnvrelem1  24616  ftc1cn  24642  mdegldg  24662  plyeq0  24803  plyaddlem1  24805  plymullem1  24806  ulmdv  24993  dchrelbas2  25815  dchrghm  25834  uhgrfun  26853  vdegp1ai  27320  vdegp1bi  27321  wlkres  27454  sspg  28507  ssps  28509  sspn  28515  htthlem  28696  fmptcof2  30404  fnpreimac  30418  curry2ima  30446  offinsupp1  30465  fpwrelmapffslem  30470  swrdrn2  30630  xrge0tsmsd  30694  cyc3co2  30784  tocyccntz  30788  rmfsupp2  30868  lbsdiflsp0  31024  fedgmullem1  31027  fedgmullem2  31028  esumpfinvallem  31335  sibfof  31600  sitgclg  31602  eulerpartlemd  31626  eulerpartlemgu  31637  eulerpartlemgf  31639  dstrvprob  31731  dstfrvel  31733  orvclteinc  31735  spthcycl  32378  cvmliftmolem1  32530  cvmliftlem3  32536  cvmliftlem10  32543  cvmliftlem13  32545  cvmlift2lem9  32560  cvmlift3lem6  32573  cvmlift3lem7  32574  satefvfmla0  32667  satefvfmla1  32674  msubrn  32778  mclsax  32818  mclsppslem  32832  mclspps  32833  ftc1cnnc  34968  heibor1lem  35089  grpokerinj  35173  lmhmfgima  39691  gneispacefun  40494  cncmpmax  41296  fidmfisupp  41469  limccog  41908  limsuppnfdlem  41989  climxrrelem  42037  climxrre  42038  liminfvalxr  42071  liminflimsupxrre  42105  xlimxrre  42119  dvsinax  42204  fvvolioof  42281  fvvolicof  42283  dirkercncflem2  42396  fourierdlem82  42480  subsaliuncllem  42647  fge0iccico  42659  sge0sn  42668  sge0tsms  42669  sge0cl  42670  sge0f1o  42671  sge0isum  42716  ovnovollem1  42945  ovnovollem2  42946  preimaioomnf  43004  smfresal  43070  smfres  43072  smfco  43084  isomushgr  43998  ushrisomgr  44013