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

Theorem sumeq1d 15578
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 15565 . 2 (𝐴 = 𝐵 → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶)
31, 2syl 17 1 (𝜑 → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  Σcsu 15562
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3063  df-rex 3072  df-rab 3406  df-v 3445  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-br 5104  df-opab 5166  df-mpt 5187  df-xp 5637  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6251  df-iota 6445  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-ov 7356  df-oprab 7357  df-mpo 7358  df-frecs 8208  df-wrecs 8239  df-recs 8313  df-rdg 8352  df-seq 13899  df-sum 15563
This theorem is referenced by:  sumeq12dv  15583  sumeq12rdv  15584  fsumf1o  15600  sumss  15601  fsumcllem  15609  fsumsplit1  15622  fsum1  15624  fzosump1  15629  fsump1  15633  fsum2d  15648  fsumcom2  15651  fsumshftm  15658  fsumrev2  15659  telfsumo  15679  telfsum  15681  telfsum2  15682  fsumparts  15683  fsumiun  15698  bcxmas  15712  incexclem  15713  incexc2  15715  isumsplit  15717  isum1p  15718  arisum  15737  arisum2  15738  geoser  15744  pwdif  15745  geolim  15747  geo2sum2  15751  mertenslem1  15761  mertenslem2  15762  mertens  15763  bpolydiflem  15929  efcvgfsum  15960  fprodefsum  15969  eftlub  15983  effsumlt  15985  eirrlem  16078  pwp1fsum  16265  bitsinv1  16314  bitsinvp1  16321  pcfac  16763  prmreclem4  16783  prmreclem6  16785  ovoliunlem1  24850  uniioombllem3  24933  itg11  25039  dvfsumlem1  25374  dvfsumlem4  25377  dvfsum2  25382  elplyr  25546  coeeu  25570  coeeq  25572  plyco  25586  0dgrb  25591  dvply2g  25629  vieta1lem2  25655  vieta1  25656  aaliou3lem5  25691  aaliou3lem6  25692  aaliou3lem7  25693  taylpfval  25708  pserdvlem2  25771  abelthlem6  25779  logfac  25940  advlogexp  25994  emcllem2  26330  emcllem3  26331  emcllem7  26335  harmonicbnd  26337  harmonicbnd2  26338  harmonicbnd3  26341  harmonicbnd4  26344  chtval  26443  chpval  26455  chtfl  26482  chpfl  26483  chtprm  26486  chtnprm  26487  chpp1  26488  chtdif  26491  prmorcht  26511  musum  26524  muinv  26526  logfaclbnd  26554  logfacbnd3  26555  logexprlim  26557  chtppilimlem1  26805  rplogsumlem2  26817  rpvmasumlem  26819  dchrisumlem1  26821  dchrisumlem2  26822  dchrisumlem3  26823  dchrisum  26824  dchrisum0fval  26837  dchrisum0ff  26839  dchrisum0flblem1  26840  dchrisum0lem2  26850  dchrisum0  26852  mulog2sumlem1  26866  2vmadivsumlem  26872  log2sumbnd  26876  logdivbnd  26888  selberg3lem1  26889  pntrsumbnd  26898  pntrsumbnd2  26899  pntrlog2bndlem1  26909  pntrlog2bndlem4  26912  pntpbnd1  26918  pntpbnd2  26919  pntlemf  26937  brcgr  27735  axlowdimlem16  27792  eengv  27814  finsumvtxdg2sstep  28383  eulerpartlemgs2  32849  signsvfn  33063  fsum2dsub  33089  reprval  33092  reprsuc  33097  hashrepr  33107  chpvalz  33110  chtvalz  33111  breprexplema  33112  breprexplemc  33114  breprexp  33115  breprexpnat  33116  vtsval  33119  circlemeth  33122  hgt750lemb  33138  hgt750lema  33139  tgoldbachgtda  33143  tgoldbachgt  33145  subfacval2  33650  subfaclim  33651  bccolsum  34182  knoppndvlem6  34947  mettrifi  36183  rrncmslem  36258  sticksstones6  40526  sticksstones7  40527  sticksstones8  40528  sticksstones9  40529  sticksstones10  40530  sticksstones11  40531  sticksstones12a  40532  sticksstones12  40533  sticksstones16  40537  fzosumm1  40632  k0004val  42364  binomcxplemnn0  42571  fsumnncl  43745  fsumiunss  43748  fsumsermpt  43752  sumnnodd  43803  dvnmul  44116  dvnprodlem3  44121  itgspltprt  44152  stoweidlem17  44190  stoweidlem20  44193  stirlinglem12  44258  dirkertrigeqlem1  44271  dirkertrigeqlem3  44273  fourierdlem83  44362  fourierdlem112  44391  fourierdlem113  44392  elaa2lem  44406  etransclem32  44439  sge00  44549  sge0iunmptlemre  44588  sge0reuzb  44621  meaiuninclem  44653  carageniuncllem1  44694  hoidmvlelem3  44770  nnsum3primes4  45912  nnsum3primesprm  45914  nnsum3primesgbe  45916  nnsum4primesodd  45920  nnsum4primesoddALTV  45921  wtgoldbnnsum4prm  45926  bgoldbnnsum3prm  45928  altgsumbcALT  46361  nn0sumshdiglemA  46637  nn0sumshdiglemB  46638  nn0sumshdiglem1  46639  nn0sumshdiglem2  46640
  Copyright terms: Public domain W3C validator