MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sumeq1d Structured version   Visualization version   GIF version

Theorem sumeq1d 14475
Description: Equality deduction for sum. (Contributed by NM, 1-Nov-2005.)
Hypothesis
Ref Expression
sumeq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
sumeq1d (𝜑 → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶)
Distinct variable groups:   𝐴,𝑘   𝐵,𝑘
Allowed substitution hints:   𝜑(𝑘)   𝐶(𝑘)

Proof of Theorem sumeq1d
StepHypRef Expression
1 sumeq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 sumeq1 14463 . 2 (𝐴 = 𝐵 → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶)
31, 2syl 17 1 (𝜑 → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  Σcsu 14460
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-xp 5149  df-cnv 5151  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-iota 5889  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-seq 12842  df-sum 14461
This theorem is referenced by:  sumeq12dv  14481  sumeq12rdv  14482  fsumf1o  14498  sumss  14499  fsumcllem  14507  fsum1  14520  fzosump1  14525  fsump1  14531  fsum2d  14546  fsumcom2  14549  fsumcom2OLD  14550  fsumshftm  14557  fsumrev2  14558  telfsumo  14578  telfsum  14580  telfsum2  14581  fsumparts  14582  fsumiun  14597  bcxmas  14611  incexclem  14612  incexc2  14614  isumsplit  14616  isum1p  14617  arisum  14636  arisum2  14637  geoser  14643  geolim  14645  geo2sum2  14649  mertenslem1  14660  mertenslem2  14661  mertens  14662  bpolydiflem  14829  efcvgfsum  14860  fprodefsum  14869  eftlub  14883  effsumlt  14885  eirrlem  14976  pwp1fsum  15161  bitsinv1  15211  bitsinvp1  15218  pcfac  15650  prmreclem4  15670  prmreclem6  15672  ovoliunlem1  23316  uniioombllem3  23399  itg11  23503  dvfsumlem1  23834  dvfsumlem4  23837  dvfsum2  23842  elplyr  24002  coeeu  24026  coeeq  24028  plyco  24042  0dgrb  24047  dvply2g  24085  vieta1lem2  24111  vieta1  24112  aaliou3lem5  24147  aaliou3lem6  24148  aaliou3lem7  24149  taylpfval  24164  pserdvlem2  24227  abelthlem6  24235  logfac  24392  advlogexp  24446  emcllem2  24768  emcllem3  24769  emcllem7  24773  harmonicbnd  24775  harmonicbnd2  24776  harmonicbnd3  24779  harmonicbnd4  24782  chtval  24881  chpval  24893  chtfl  24920  chpfl  24921  chtprm  24924  chtnprm  24925  chpp1  24926  chtdif  24929  prmorcht  24949  musum  24962  muinv  24964  logfaclbnd  24992  logfacbnd3  24993  logexprlim  24995  chtppilimlem1  25207  rplogsumlem2  25219  rpvmasumlem  25221  dchrisumlem1  25223  dchrisumlem2  25224  dchrisumlem3  25225  dchrisum  25226  dchrisum0fval  25239  dchrisum0ff  25241  dchrisum0flblem1  25242  dchrisum0lem2  25252  dchrisum0  25254  mulog2sumlem1  25268  2vmadivsumlem  25274  log2sumbnd  25278  logdivbnd  25290  selberg3lem1  25291  pntrsumbnd  25300  pntrsumbnd2  25301  pntrlog2bndlem1  25311  pntrlog2bndlem4  25314  pntpbnd1  25320  pntpbnd2  25321  pntlemf  25339  brcgr  25825  axlowdimlem16  25882  eengv  25904  finsumvtxdg2sstep  26501  eulerpartlemgs2  30570  signsvfn  30787  fsum2dsub  30813  reprval  30816  reprsuc  30821  hashrepr  30831  chpvalz  30834  chtvalz  30835  breprexplema  30836  breprexplemc  30838  breprexp  30839  breprexpnat  30840  vtsval  30843  circlemeth  30846  hgt750lemb  30862  hgt750lema  30863  tgoldbachgtda  30867  tgoldbachgt  30869  subfacval2  31295  subfaclim  31296  bccolsum  31751  knoppndvlem6  32633  mettrifi  33683  rrncmslem  33761  k0004val  38765  binomcxplemnn0  38865  fsumnncl  40121  fsumsplit1  40122  fsumiunss  40125  fsumsermpt  40129  sumnnodd  40180  dvnmul  40476  dvnprodlem3  40481  itgspltprt  40513  stoweidlem17  40552  stoweidlem20  40555  stirlinglem12  40620  dirkertrigeqlem1  40633  dirkertrigeqlem3  40635  fourierdlem83  40724  fourierdlem112  40753  fourierdlem113  40754  elaa2lem  40768  etransclem32  40801  sge00  40911  sge0iunmptlemre  40950  sge0reuzb  40983  meaiuninclem  41015  carageniuncllem1  41056  hoidmvlelem3  41132  pwdif  41826  nnsum3primes4  42001  nnsum3primesprm  42003  nnsum3primesgbe  42005  nnsum4primesodd  42009  nnsum4primesoddALTV  42010  wtgoldbnnsum4prm  42015  bgoldbnnsum3prm  42017  altgsumbcALT  42456  nn0sumshdiglemA  42738  nn0sumshdiglemB  42739  nn0sumshdiglem1  42740  nn0sumshdiglem2  42741
  Copyright terms: Public domain W3C validator