Theorem ffund 6727

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

Syntax hints:   → wi 4  Fun wfun 6543  ⟶wf 6545

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 206  df-an 395  df-fn 6552  df-f 6553

This theorem is referenced by:  fofun  6811  fssrescdmd  7135  fmptco  7138  funfvima2d  7244  smores2  8375  elmapfun  8885  fidmfisupp  9398  fdmfifsupp  9400  fsuppmptif  9424  fsuppco2  9428  fsuppcor  9429  ordtypelem8  9550  ordtypelem9  9551  ordtypelem10  9552  unxpwdom2  9613  fpwwe2  10668  swrdwrdsymb  14648  mrcuni  17604  frmdss2  18823  cntzmhm2  19305  frgpupval  19741  gsumzadd  19889  gsumpt  19929  gsum2dlem2  19938  dprd2da  20011  lmhmpreima  20945  lmhmlsp  20946  rhmpreimaidl  21184  cygznlem2  21519  frlmsslsp  21747  frlmup1  21749  frlmup4  21752  lindff1  21771  lindfrn  21772  psrelbasfun  21897  mvrcl  21954  evlslem3  22048  evlseu  22051  mpfind  22075  mhpmulcl  22096  psdmul  22113  gsumply1subr  22176  cnclsi  23220  cncnp  23228  paste  23242  connima  23373  1stcfb  23393  1stccnp  23410  1stckgenlem  23501  txcnpi  23556  txcnp  23568  xkoco2cn  23606  fmfnfmlem2  23903  lmflf  23953  txflf  23954  cnextcn  24015  clssubg  24057  ghmcnp  24063  metustid  24507  metustexhalf  24509  isngp2  24550  pi1xfrval  25025  pi1coval  25031  iscfil2  25238  rrxcph  25364  ismbfd  25612  ellimc2  25850  ellimc3  25852  dvres3  25886  dvres3a  25887  dvcnv  25953  dvcnvrelem1  25994  ftc1cn  26022  mdegldg  26046  plyeq0  26190  plyaddlem1  26192  plymullem1  26193  ulmdv  26384  dchrelbas2  27215  dchrghm  27234  uhgrfun  28951  vdegp1ai  29422  vdegp1bi  29423  wlkres  29556  sspg  30610  ssps  30612  sspn  30618  htthlem  30799  fmptcof2  32524  fnpreimac  32538  curry2ima  32570  offinsupp1  32591  fpwrelmapffslem  32596  swrdrn2  32764  pwrssmgc  32816  gsumhashmul  32860  xrge0tsmsd  32861  wrdpmtrlast  32906  cyc3co2  32953  tocyccntz  32957  rmfsupp2  33038  elrspunidl  33240  rhmimaidl  33244  ig1pmindeg  33403  ply1degltdimlem  33451  lbsdiflsp0  33455  fedgmullem1  33458  fedgmullem2  33459  evls1fldgencl  33489  rhmpreimacnlem  33616  esumpfinvallem  33824  sibfof  34091  sitgclg  34093  eulerpartlemd  34117  eulerpartlemgu  34128  eulerpartlemgf  34130  dstrvprob  34222  dstfrvel  34224  orvclteinc  34226  spthcycl  34870  cvmliftmolem1  35022  cvmliftlem3  35028  cvmliftlem10  35035  cvmliftlem13  35037  cvmlift2lem9  35052  cvmlift3lem6  35065  cvmlift3lem7  35066  satefvfmla0  35159  satefvfmla1  35166  msubrn  35270  mclsax  35310  mclsppslem  35324  mclspps  35325  ftc1cnnc  37296  heibor1lem  37413  grpokerinj  37497  aks6d1c3  41726  aks6d1c4  41727  sticksstones1  41749  aks6d1c6lem2  41774  rhmqusspan  41788  aks5lem2  41790  imacrhmcl  41889  evlsvvvallem  41929  evlselvlem  41954  evlselv  41955  lmhmfgima  42650  cantnfub  42892  onnog  43001  gneispacefun  43709  cncmpmax  44536  limccog  45146  limsuppnfdlem  45227  climxrrelem  45275  climxrre  45276  liminfvalxr  45309  liminflimsupxrre  45343  xlimxrre  45357  dvsinax  45439  fvvolioof  45515  fvvolicof  45517  dirkercncflem2  45630  fourierdlem82  45714  subsaliuncllem  45883  fge0iccico  45896  sge0sn  45905  sge0tsms  45906  sge0cl  45907  sge0f1o  45908  sge0isum  45953  ovnovollem1  46182  ovnovollem2  46183  preimaioomnf  46245  smfresal  46314  smfres  46316  smfco  46328  fcoreslem1  46583  fcoreslem2  46584  fcores  46587  gricushgr  47369  ushggricedg  47379  cnneiima  48121  sepfsepc  48132