Theorem ffund 6666

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

Syntax hints:   → wi 4  Fun wfun 6486  ⟶wf 6488

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 6495  df-f 6496

This theorem is referenced by:  fofun  6747  fssrescdmd  7073  fmptco  7076  funfvima2d  7180  smores2  8287  elmapfun  8806  fidmfisupp  9278  fdmfifsupp  9281  fsuppmptif  9305  fsuppco2  9309  fsuppcor  9310  ordtypelem8  9433  ordtypelem9  9434  ordtypelem10  9435  unxpwdom2  9496  fpwwe2  10557  swrdwrdsymb  14616  mrcuni  17578  frmdss2  18822  cntzmhm2  19308  frgpupval  19740  gsumzadd  19888  gsumpt  19928  gsum2dlem2  19937  dprd2da  20010  lmhmpreima  21035  lmhmlsp  21036  rhmpreimaidl  21267  cygznlem2  21558  frlmsslsp  21786  frlmup1  21788  frlmup4  21791  lindff1  21810  lindfrn  21811  psrelbasfun  21925  mvrcl  21980  evlslem3  22068  evlseu  22071  evlsvvvallem  22079  mpfind  22103  mhpmulcl  22125  psdmul  22142  gsumply1subr  22207  cnclsi  23247  cncnp  23255  paste  23269  connima  23400  1stcfb  23420  1stccnp  23437  1stckgenlem  23528  txcnpi  23583  txcnp  23595  xkoco2cn  23633  fmfnfmlem2  23930  lmflf  23980  txflf  23981  cnextcn  24042  clssubg  24084  ghmcnp  24090  metustid  24529  metustexhalf  24531  isngp2  24572  pi1xfrval  25031  pi1coval  25037  iscfil2  25243  rrxcph  25369  ismbfd  25616  ellimc2  25854  ellimc3  25856  dvres3  25890  dvres3a  25891  dvcnv  25954  dvcnvrelem1  25994  ftc1cn  26020  mdegldg  26041  plyeq0  26186  plyaddlem1  26188  plymullem1  26189  ulmdv  26381  dchrelbas2  27214  dchrghm  27233  uhgrfun  29149  vdegp1ai  29620  vdegp1bi  29621  wlkres  29752  sspg  30814  ssps  30816  sspn  30822  htthlem  31003  fmptcof2  32745  fnpreimac  32758  curry2ima  32797  offinsupp1  32814  fpwrelmapffslem  32820  indfsd  32943  swrdrn2  33029  pwrssmgc  33075  gsumhashmul  33143  xrge0tsmsd  33149  wrdpmtrlast  33169  cyc3co2  33216  tocyccntz  33220  rmfsupp2  33314  elrgspnlem1  33318  elrgspnlem2  33319  elrgspnlem3  33320  elrgspnlem4  33321  elrgspnsubrunlem1  33323  elrgspnsubrunlem2  33324  elrspunidl  33503  rhmimaidl  33507  ig1pmindeg  33677  extvfvcl  33695  mplmulmvr  33698  evlextv  33701  psrmonprod  33711  esplylem  33725  esplympl  33726  esplymhp  33727  esplyfv1  33728  ply1degltdimlem  33782  lbsdiflsp0  33786  fedgmullem1  33789  fedgmullem2  33790  evls1fldgencl  33830  fldextrspunlsp  33834  extdgfialglem1  33852  rhmpreimacnlem  34044  esumpfinvallem  34234  sibfof  34500  sitgclg  34502  eulerpartlemd  34526  eulerpartlemgu  34537  eulerpartlemgf  34539  dstrvprob  34632  dstfrvel  34634  orvclteinc  34636  spthcycl  35327  cvmliftmolem1  35479  cvmliftlem3  35485  cvmliftlem10  35492  cvmliftlem13  35494  cvmlift2lem9  35509  cvmlift3lem6  35522  cvmlift3lem7  35523  satefvfmla0  35616  satefvfmla1  35623  msubrn  35727  mclsax  35767  mclsppslem  35781  mclspps  35782  weiunfr  36665  ftc1cnnc  38027  heibor1lem  38144  grpokerinj  38228  aks6d1c3  42576  aks6d1c4  42577  sticksstones1  42599  aks6d1c6lem2  42624  rhmqusspan  42638  aks5lem2  42640  imacrhmcl  42973  evlselvlem  43033  evlselv  43034  lmhmfgima  43530  cantnfub  43767  onnoxpg  43874  gneispacefun  44582  relpfrlem  45398  cncmpmax  45481  limccog  46068  limsuppnfdlem  46147  climxrrelem  46195  climxrre  46196  liminfvalxr  46229  liminflimsupxrre  46263  xlimxrre  46277  dvsinax  46359  fvvolioof  46435  fvvolicof  46437  dirkercncflem2  46550  fourierdlem82  46634  subsaliuncllem  46803  fge0iccico  46816  sge0sn  46825  sge0tsms  46826  sge0cl  46827  sge0f1o  46828  sge0isum  46873  ovnovollem1  47102  ovnovollem2  47103  preimaioomnf  47165  smfresal  47234  smfres  47236  smfco  47248  fcoreslem1  47523  fcoreslem2  47524  fcores  47527  gricushgr  48405  ushggricedg  48415  uspgrlimlem4  48479  ffvbr  49343  cnneiima  49404  sepfsepc  49415  imaf1co  49642