Theorem ffund 6508

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

Syntax hints:   → wi 4  Fun wfun 6333  ⟶wf 6335

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 210  df-an 400  df-fn 6342  df-f 6343

This theorem is referenced by:  fofun  6593  fmptco  6901  funfvima2d  7005  smores2  8020  elmapfun  8476  fdmfifsupp  8916  fsuppmptif  8936  fsuppco2  8940  fsuppcor  8941  ordtypelem8  9062  ordtypelem9  9063  ordtypelem10  9064  unxpwdom2  9125  fpwwe2  10143  swrdwrdsymb  14113  mrcuni  16995  frmdss2  18144  cntzmhm2  18588  frgpupval  19018  gsumzadd  19161  gsumpt  19201  gsum2dlem2  19210  dprd2da  19283  lmhmpreima  19939  lmhmlsp  19940  cygznlem2  20387  frlmsslsp  20612  frlmup1  20614  frlmup4  20617  lindff1  20636  lindfrn  20637  psrelbasfun  20759  mvrcl  20831  evlslem3  20894  evlseu  20897  mpfind  20921  mhpmulcl  20943  gsumply1subr  21009  cnclsi  22023  cncnp  22031  paste  22045  connima  22176  1stcfb  22196  1stccnp  22213  1stckgenlem  22304  txcnpi  22359  txcnp  22371  xkoco2cn  22409  fmfnfmlem2  22706  lmflf  22756  txflf  22757  cnextcn  22818  clssubg  22860  ghmcnp  22866  metustid  23307  metustexhalf  23309  isngp2  23350  pi1xfrval  23806  pi1coval  23812  iscfil2  24018  rrxcph  24144  ismbfd  24391  ellimc2  24629  ellimc3  24631  dvres3  24665  dvres3a  24666  dvcnv  24729  dvcnvrelem1  24769  ftc1cn  24795  mdegldg  24819  plyeq0  24960  plyaddlem1  24962  plymullem1  24963  ulmdv  25150  dchrelbas2  25973  dchrghm  25992  uhgrfun  27011  vdegp1ai  27478  vdegp1bi  27479  wlkres  27612  sspg  28663  ssps  28665  sspn  28671  htthlem  28852  fmptcof2  30569  fnpreimac  30583  curry2ima  30616  offinsupp1  30637  fpwrelmapffslem  30642  swrdrn2  30801  pwrssmgc  30855  gsumhashmul  30893  xrge0tsmsd  30894  cyc3co2  30984  tocyccntz  30988  rmfsupp2  31069  rhmpreimaidl  31175  elrspunidl  31178  rhmimaidl  31181  lbsdiflsp0  31279  fedgmullem1  31282  fedgmullem2  31283  rhmpreimacnlem  31406  esumpfinvallem  31612  sibfof  31877  sitgclg  31879  eulerpartlemd  31903  eulerpartlemgu  31914  eulerpartlemgf  31916  dstrvprob  32008  dstfrvel  32010  orvclteinc  32012  spthcycl  32662  cvmliftmolem1  32814  cvmliftlem3  32820  cvmliftlem10  32827  cvmliftlem13  32829  cvmlift2lem9  32844  cvmlift3lem6  32857  cvmlift3lem7  32858  satefvfmla0  32951  satefvfmla1  32958  msubrn  33062  mclsax  33102  mclsppslem  33116  mclspps  33117  ftc1cnnc  35472  heibor1lem  35590  grpokerinj  35674  sticksstones1  39708  lmhmfgima  40481  gneispacefun  41293  cncmpmax  42113  fidmfisupp  42277  limccog  42703  limsuppnfdlem  42784  climxrrelem  42832  climxrre  42833  liminfvalxr  42866  liminflimsupxrre  42900  xlimxrre  42914  dvsinax  42996  fvvolioof  43072  fvvolicof  43074  dirkercncflem2  43187  fourierdlem82  43271  subsaliuncllem  43438  fge0iccico  43450  sge0sn  43459  sge0tsms  43460  sge0cl  43461  sge0f1o  43462  sge0isum  43507  ovnovollem1  43736  ovnovollem2  43737  preimaioomnf  43795  smfresal  43861  smfres  43863  smfco  43875  fcoreslem1  44095  fcoreslem2  44096  fcores  44099  isomushgr  44812  ushrisomgr  44827  cnneiima  45732  sepfsepc  45743