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

Theorem sumeq1d 15050
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 15037 . 2 (𝐴 = 𝐵 → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶)
31, 2syl 17 1 (𝜑 → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1531  Σcsu 15034
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-xp 5554  df-cnv 5556  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-iota 6307  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-ov 7151  df-oprab 7152  df-mpo 7153  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-seq 13362  df-sum 15035
This theorem is referenced by:  sumeq12dv  15055  sumeq12rdv  15056  fsumf1o  15072  sumss  15073  fsumcllem  15081  fsum1  15094  fzosump1  15099  fsump1  15103  fsum2d  15118  fsumcom2  15121  fsumshftm  15128  fsumrev2  15129  telfsumo  15149  telfsum  15151  telfsum2  15152  fsumparts  15153  fsumiun  15168  bcxmas  15182  incexclem  15183  incexc2  15185  isumsplit  15187  isum1p  15188  arisum  15207  arisum2  15208  geoser  15214  pwdif  15215  geolim  15218  geo2sum2  15222  mertenslem1  15232  mertenslem2  15233  mertens  15234  bpolydiflem  15400  efcvgfsum  15431  fprodefsum  15440  eftlub  15454  effsumlt  15456  eirrlem  15549  pwp1fsum  15734  bitsinv1  15783  bitsinvp1  15790  pcfac  16227  prmreclem4  16247  prmreclem6  16249  ovoliunlem1  24095  uniioombllem3  24178  itg11  24284  dvfsumlem1  24615  dvfsumlem4  24618  dvfsum2  24623  elplyr  24783  coeeu  24807  coeeq  24809  plyco  24823  0dgrb  24828  dvply2g  24866  vieta1lem2  24892  vieta1  24893  aaliou3lem5  24928  aaliou3lem6  24929  aaliou3lem7  24930  taylpfval  24945  pserdvlem2  25008  abelthlem6  25016  logfac  25176  advlogexp  25230  emcllem2  25566  emcllem3  25567  emcllem7  25571  harmonicbnd  25573  harmonicbnd2  25574  harmonicbnd3  25577  harmonicbnd4  25580  chtval  25679  chpval  25691  chtfl  25718  chpfl  25719  chtprm  25722  chtnprm  25723  chpp1  25724  chtdif  25727  prmorcht  25747  musum  25760  muinv  25762  logfaclbnd  25790  logfacbnd3  25791  logexprlim  25793  chtppilimlem1  26041  rplogsumlem2  26053  rpvmasumlem  26055  dchrisumlem1  26057  dchrisumlem2  26058  dchrisumlem3  26059  dchrisum  26060  dchrisum0fval  26073  dchrisum0ff  26075  dchrisum0flblem1  26076  dchrisum0lem2  26086  dchrisum0  26088  mulog2sumlem1  26102  2vmadivsumlem  26108  log2sumbnd  26112  logdivbnd  26124  selberg3lem1  26125  pntrsumbnd  26134  pntrsumbnd2  26135  pntrlog2bndlem1  26145  pntrlog2bndlem4  26148  pntpbnd1  26154  pntpbnd2  26155  pntlemf  26173  brcgr  26678  axlowdimlem16  26735  eengv  26757  finsumvtxdg2sstep  27323  eulerpartlemgs2  31631  signsvfn  31845  fsum2dsub  31871  reprval  31874  reprsuc  31879  hashrepr  31889  chpvalz  31892  chtvalz  31893  breprexplema  31894  breprexplemc  31896  breprexp  31897  breprexpnat  31898  vtsval  31901  circlemeth  31904  hgt750lemb  31920  hgt750lema  31921  tgoldbachgtda  31925  tgoldbachgt  31927  subfacval2  32427  subfaclim  32428  bccolsum  32964  knoppndvlem6  33849  mettrifi  35024  rrncmslem  35102  fzosumm1  39116  k0004val  40490  binomcxplemnn0  40671  fsumnncl  41841  fsumsplit1  41842  fsumiunss  41845  fsumsermpt  41849  sumnnodd  41900  dvnmul  42217  dvnprodlem3  42222  itgspltprt  42253  stoweidlem17  42292  stoweidlem20  42295  stirlinglem12  42360  dirkertrigeqlem1  42373  dirkertrigeqlem3  42375  fourierdlem83  42464  fourierdlem112  42493  fourierdlem113  42494  elaa2lem  42508  etransclem32  42541  sge00  42648  sge0iunmptlemre  42687  sge0reuzb  42720  meaiuninclem  42752  carageniuncllem1  42793  hoidmvlelem3  42869  nnsum3primes4  43943  nnsum3primesprm  43945  nnsum3primesgbe  43947  nnsum4primesodd  43951  nnsum4primesoddALTV  43952  wtgoldbnnsum4prm  43957  bgoldbnnsum3prm  43959  altgsumbcALT  44391  nn0sumshdiglemA  44669  nn0sumshdiglemB  44670  nn0sumshdiglem1  44671  nn0sumshdiglem2  44672
  Copyright terms: Public domain W3C validator