Theorem ffund 6717

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

This proof depends on syntax axioms:   → wi 4  Fun wfun 6537  ⟶wf 6539

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fn 6546  df-f 6547

This theorem is used by:  fofun  6800  fssrescdmd  7129  fmptco  7132  funfvima2d  7237  smores2  8350  elmapfun  8872  fidmfisupp  9342  fdmfifsupp  9345  fsuppmptif  9369  fsuppco2  9373  fsuppcor  9374  ordtypelem8  9497  ordtypelem9  9498  ordtypelem10  9499  unxpwdom2  9560  fpwwe2  10646  swrdwrdsymb  14724  mrcuni  17702  frmdss2  18953  cntzmhm2  19443  frgpupval  19875  gsumzadd  20023  gsumpt  20063  gsum2dlem2  20072  dprd2da  20145  lmhmpreima  21206  lmhmlsp  21207  rhmpreimaidl  21453  cygznlem2  21755  frlmsslsp  21983  frlmup1  21985  frlmup4  21988  lindff1  22007  lindfrn  22008  psrelbasfun  22123  mvrcl  22178  evlslem3  22268  evlseu  22271  evlsvvvallem  22279  mpfind  22303  mhpmulcl  22349  psdmul  22366  gsumply1subr  22430  cnclsi  23466  cncnp  23474  paste  23488  connima  23619  1stcfb  23639  1stccnp  23656  1stckgenlem  23747  txcnpi  23802  txcnp  23814  xkoco2cn  23852  fmfnfmlem2  24149  lmflf  24199  txflf  24200  cnextcn  24261  clssubg  24303  ghmcnp  24309  metustid  24748  metustexhalf  24750  isngp2  24791  pi1xfrval  25250  pi1coval  25256  iscfil2  25462  rrxcph  25588  ismbfd  25835  ellimc2  26073  ellimc3  26075  dvres3  26109  dvres3a  26110  dvcnv  26173  dvcnvrelem1  26213  ftc1cn  26239  mdegldg  26260  plyeq0  26405  plyaddlem1  26407  plymullem1  26408  ulmdv  26603  dchrelbas2  27438  dchrghm  27457  uhgrfun  29453  vdegp1ai  29923  vdegp1bi  29924  wlkres  30055  sspg  31117  ssps  31119  sspn  31125  htthlem  31306  fmptcof2  33039  fnpreimac  33052  curry2ima  33091  offinsupp1  33108  fpwrelmapffslem  33114  indfsd  33225  swrdrn2  33307  pwrssmgc  33351  gsumhashmul  33418  xrge0tsmsd  33424  wrdpmtrlast  33444  cyc3co2  33491  tocyccntz  33495  rmfsupp2  33588  elrgspnlem1  33593  elrgspnlem2  33594  elrgspnlem3  33595  elrgspnlem4  33596  elrgspnsubrunlem1  33598  elrgspnsubrunlem2  33599  elrspunidl  33767  rhmimaidl  33771  ig1pmindeg  33923  selvascl  33938  extvfvcl  33957  mplmulmvr  33960  evlextv  33963  psrmonprod  33973  esplylem  33987  esplympl  33988  esplymhp  33989  esplyfv1  33990  ply1degltdimlem  34043  lbsdiflsp0  34047  fedgmullem1  34050  fedgmullem2  34051  evls1fldgencl  34091  fldextrspunlsp  34095  extdgfialglem1  34113  rhmpreimacnlem  34305  esumpfinvallem  34495  sibfof  34761  sitgclg  34763  eulerpartlemd  34787  eulerpartlemgu  34798  eulerpartlemgf  34800  dstrvprob  34893  dstfrvel  34895  orvclteinc  34897  spthcycl  35641  cvmliftmolem1  35793  cvmliftlem3  35799  cvmliftlem10  35806  cvmliftlem13  35808  cvmlift2lem9  35823  cvmlift3lem6  35836  cvmlift3lem7  35837  satefvfmla0  35930  satefvfmla1  35937  msubrn  36041  mclsax  36081  mclsppslem  36095  mclspps  36096  weiunfr  37018  ftc1cnnc  38383  heibor1lem  38500  grpokerinj  38584  aks6d1c3  42930  aks6d1c4  42931  sticksstones1  42953  aks6d1c6lem2  42978  rhmqusspan  42992  aks5lem2  42994  imacrhmcl  43328  evlselvlem  43360  evlselv  43361  lmhmfgima  43851  cantnfub  44088  onnoxpg  44195  gneispacefun  44903  relpfrlem  45702  cncmpmax  45792  limccog  46376  limsuppnfdlem  46455  climxrrelem  46503  climxrre  46504  liminfvalxr  46537  liminflimsupxrre  46571  xlimxrre  46585  dvsinax  46667  fvvolioof  46743  fvvolicof  46745  dirkercncflem2  46858  fourierdlem82  46942  fourierdlem113  46973  subsaliuncllem  47111  fge0iccico  47124  sge0sn  47133  sge0tsms  47134  sge0cl  47135  sge0f1o  47136  sge0isum  47181  ovnovollem1  47410  ovnovollem2  47411  preimaioomnf  47473  smfresal  47542  smfres  47544  smfco  47556  fcoreslem1  47840  fcoreslem2  47841  fcores  47844  gricushgr  48722  ushggricedg  48732  uspgrlimlem4  48796  ffvbr  49674  cnneiima  49735  sepfsepc  49746  imaf1co  49973