Theorem ffund 6710

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

Syntax hints:   → wi 4  Fun wfun 6525  ⟶wf 6527

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 6534  df-f 6535

This theorem is referenced by:  fofun  6791  fssrescdmd  7116  fmptco  7119  funfvima2d  7224  smores2  8368  elmapfun  8880  fidmfisupp  9384  fdmfifsupp  9387  fsuppmptif  9411  fsuppco2  9415  fsuppcor  9416  ordtypelem8  9539  ordtypelem9  9540  ordtypelem10  9541  unxpwdom2  9602  fpwwe2  10657  swrdwrdsymb  14680  mrcuni  17633  frmdss2  18841  cntzmhm2  19325  frgpupval  19755  gsumzadd  19903  gsumpt  19943  gsum2dlem2  19952  dprd2da  20025  lmhmpreima  21006  lmhmlsp  21007  rhmpreimaidl  21238  cygznlem2  21529  frlmsslsp  21756  frlmup1  21758  frlmup4  21761  lindff1  21780  lindfrn  21781  psrelbasfun  21895  mvrcl  21952  evlslem3  22038  evlseu  22041  mpfind  22065  mhpmulcl  22087  psdmul  22104  gsumply1subr  22169  cnclsi  23210  cncnp  23218  paste  23232  connima  23363  1stcfb  23383  1stccnp  23400  1stckgenlem  23491  txcnpi  23546  txcnp  23558  xkoco2cn  23596  fmfnfmlem2  23893  lmflf  23943  txflf  23944  cnextcn  24005  clssubg  24047  ghmcnp  24053  metustid  24493  metustexhalf  24495  isngp2  24536  pi1xfrval  25005  pi1coval  25011  iscfil2  25218  rrxcph  25344  ismbfd  25592  ellimc2  25830  ellimc3  25832  dvres3  25866  dvres3a  25867  dvcnv  25933  dvcnvrelem1  25974  ftc1cn  26002  mdegldg  26023  plyeq0  26168  plyaddlem1  26170  plymullem1  26171  ulmdv  26364  dchrelbas2  27200  dchrghm  27219  uhgrfun  29045  vdegp1ai  29516  vdegp1bi  29517  wlkres  29650  sspg  30709  ssps  30711  sspn  30717  htthlem  30898  fmptcof2  32635  fnpreimac  32649  curry2ima  32686  offinsupp1  32704  fpwrelmapffslem  32709  swrdrn2  32930  pwrssmgc  32980  gsumhashmul  33055  xrge0tsmsd  33056  wrdpmtrlast  33104  cyc3co2  33151  tocyccntz  33155  rmfsupp2  33233  elrgspnlem1  33237  elrgspnlem2  33238  elrgspnlem3  33239  elrgspnlem4  33240  elrgspnsubrunlem1  33242  elrgspnsubrunlem2  33243  elrspunidl  33443  rhmimaidl  33447  ig1pmindeg  33611  ply1degltdimlem  33662  lbsdiflsp0  33666  fedgmullem1  33669  fedgmullem2  33670  evls1fldgencl  33711  fldextrspunlsp  33715  rhmpreimacnlem  33915  esumpfinvallem  34105  sibfof  34372  sitgclg  34374  eulerpartlemd  34398  eulerpartlemgu  34409  eulerpartlemgf  34411  dstrvprob  34504  dstfrvel  34506  orvclteinc  34508  spthcycl  35151  cvmliftmolem1  35303  cvmliftlem3  35309  cvmliftlem10  35316  cvmliftlem13  35318  cvmlift2lem9  35333  cvmlift3lem6  35346  cvmlift3lem7  35347  satefvfmla0  35440  satefvfmla1  35447  msubrn  35551  mclsax  35591  mclsppslem  35605  mclspps  35606  weiunfr  36485  ftc1cnnc  37716  heibor1lem  37833  grpokerinj  37917  aks6d1c3  42136  aks6d1c4  42137  sticksstones1  42159  aks6d1c6lem2  42184  rhmqusspan  42198  aks5lem2  42200  imacrhmcl  42537  evlsvvvallem  42584  evlselvlem  42609  evlselv  42610  lmhmfgima  43108  cantnfub  43345  onnog  43453  gneispacefun  44161  relpfrlem  44978  cncmpmax  45056  limccog  45649  limsuppnfdlem  45730  climxrrelem  45778  climxrre  45779  liminfvalxr  45812  liminflimsupxrre  45846  xlimxrre  45860  dvsinax  45942  fvvolioof  46018  fvvolicof  46020  dirkercncflem2  46133  fourierdlem82  46217  subsaliuncllem  46386  fge0iccico  46399  sge0sn  46408  sge0tsms  46409  sge0cl  46410  sge0f1o  46411  sge0isum  46456  ovnovollem1  46685  ovnovollem2  46686  preimaioomnf  46748  smfresal  46817  smfres  46819  smfco  46831  fcoreslem1  47092  fcoreslem2  47093  fcores  47096  gricushgr  47930  ushggricedg  47940  uspgrlimlem4  48003  cnneiima  48891  sepfsepc  48902  imaf1co  49095