Theorem ffund 6751

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

Syntax hints:   → wi 4  Fun wfun 6567  ⟶wf 6569

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 6576  df-f 6577

This theorem is referenced by:  fofun  6835  fssrescdmd  7160  fmptco  7163  funfvima2d  7269  smores2  8410  elmapfun  8924  fidmfisupp  9442  fdmfifsupp  9444  fsuppmptif  9468  fsuppco2  9472  fsuppcor  9473  ordtypelem8  9594  ordtypelem9  9595  ordtypelem10  9596  unxpwdom2  9657  fpwwe2  10712  swrdwrdsymb  14710  mrcuni  17679  frmdss2  18898  cntzmhm2  19382  frgpupval  19816  gsumzadd  19964  gsumpt  20004  gsum2dlem2  20013  dprd2da  20086  lmhmpreima  21070  lmhmlsp  21071  rhmpreimaidl  21310  cygznlem2  21610  frlmsslsp  21839  frlmup1  21841  frlmup4  21844  lindff1  21863  lindfrn  21864  psrelbasfun  21978  mvrcl  22035  evlslem3  22127  evlseu  22130  mpfind  22154  mhpmulcl  22176  psdmul  22193  gsumply1subr  22256  cnclsi  23301  cncnp  23309  paste  23323  connima  23454  1stcfb  23474  1stccnp  23491  1stckgenlem  23582  txcnpi  23637  txcnp  23649  xkoco2cn  23687  fmfnfmlem2  23984  lmflf  24034  txflf  24035  cnextcn  24096  clssubg  24138  ghmcnp  24144  metustid  24588  metustexhalf  24590  isngp2  24631  pi1xfrval  25106  pi1coval  25112  iscfil2  25319  rrxcph  25445  ismbfd  25693  ellimc2  25932  ellimc3  25934  dvres3  25968  dvres3a  25969  dvcnv  26035  dvcnvrelem1  26076  ftc1cn  26104  mdegldg  26125  plyeq0  26270  plyaddlem1  26272  plymullem1  26273  ulmdv  26464  dchrelbas2  27299  dchrghm  27318  uhgrfun  29101  vdegp1ai  29572  vdegp1bi  29573  wlkres  29706  sspg  30760  ssps  30762  sspn  30768  htthlem  30949  fmptcof2  32675  fnpreimac  32689  curry2ima  32720  offinsupp1  32741  fpwrelmapffslem  32746  swrdrn2  32921  pwrssmgc  32973  gsumhashmul  33040  xrge0tsmsd  33041  wrdpmtrlast  33086  cyc3co2  33133  tocyccntz  33137  rmfsupp2  33218  elrspunidl  33421  rhmimaidl  33425  ig1pmindeg  33587  ply1degltdimlem  33635  lbsdiflsp0  33639  fedgmullem1  33642  fedgmullem2  33643  evls1fldgencl  33680  rhmpreimacnlem  33830  esumpfinvallem  34038  sibfof  34305  sitgclg  34307  eulerpartlemd  34331  eulerpartlemgu  34342  eulerpartlemgf  34344  dstrvprob  34436  dstfrvel  34438  orvclteinc  34440  spthcycl  35097  cvmliftmolem1  35249  cvmliftlem3  35255  cvmliftlem10  35262  cvmliftlem13  35264  cvmlift2lem9  35279  cvmlift3lem6  35292  cvmlift3lem7  35293  satefvfmla0  35386  satefvfmla1  35393  msubrn  35497  mclsax  35537  mclsppslem  35551  mclspps  35552  weiunfr  36433  ftc1cnnc  37652  heibor1lem  37769  grpokerinj  37853  aks6d1c3  42080  aks6d1c4  42081  sticksstones1  42103  aks6d1c6lem2  42128  rhmqusspan  42142  aks5lem2  42144  imacrhmcl  42469  evlsvvvallem  42516  evlselvlem  42541  evlselv  42542  lmhmfgima  43041  cantnfub  43283  onnog  43391  gneispacefun  44099  cncmpmax  44932  limccog  45541  limsuppnfdlem  45622  climxrrelem  45670  climxrre  45671  liminfvalxr  45704  liminflimsupxrre  45738  xlimxrre  45752  dvsinax  45834  fvvolioof  45910  fvvolicof  45912  dirkercncflem2  46025  fourierdlem82  46109  subsaliuncllem  46278  fge0iccico  46291  sge0sn  46300  sge0tsms  46301  sge0cl  46302  sge0f1o  46303  sge0isum  46348  ovnovollem1  46577  ovnovollem2  46578  preimaioomnf  46640  smfresal  46709  smfres  46711  smfco  46723  fcoreslem1  46978  fcoreslem2  46979  fcores  46982  gricushgr  47770  ushggricedg  47780  uspgrlimlem4  47815  cnneiima  48596  sepfsepc  48607