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

Theorem sumeq1d 14772
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 14760 . 2 (𝐴 = 𝐵 → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶)
31, 2syl 17 1 (𝜑 → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1653  Σcsu 14757
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3387  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4116  df-if 4278  df-sn 4369  df-pr 4371  df-op 4375  df-uni 4629  df-br 4844  df-opab 4906  df-mpt 4923  df-xp 5318  df-cnv 5320  df-dm 5322  df-rn 5323  df-res 5324  df-ima 5325  df-pred 5898  df-iota 6064  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-ov 6881  df-oprab 6882  df-mpt2 6883  df-wrecs 7645  df-recs 7707  df-rdg 7745  df-seq 13056  df-sum 14758
This theorem is referenced by:  sumeq12dv  14778  sumeq12rdv  14779  fsumf1o  14795  sumss  14796  fsumcllem  14804  fsum1  14817  fzosump1  14822  fsump1  14826  fsum2d  14841  fsumcom2  14844  fsumshftm  14851  fsumrev2  14852  telfsumo  14872  telfsum  14874  telfsum2  14875  fsumparts  14876  fsumiun  14891  bcxmas  14905  incexclem  14906  incexc2  14908  isumsplit  14910  isum1p  14911  arisum  14930  arisum2  14931  geoser  14937  geolim  14939  geo2sum2  14943  mertenslem1  14953  mertenslem2  14954  mertens  14955  bpolydiflem  15121  efcvgfsum  15152  fprodefsum  15161  eftlub  15175  effsumlt  15177  eirrlem  15268  pwp1fsum  15450  bitsinv1  15499  bitsinvp1  15506  pcfac  15936  prmreclem4  15956  prmreclem6  15958  ovoliunlem1  23610  uniioombllem3  23693  itg11  23799  dvfsumlem1  24130  dvfsumlem4  24133  dvfsum2  24138  elplyr  24298  coeeu  24322  coeeq  24324  plyco  24338  0dgrb  24343  dvply2g  24381  vieta1lem2  24407  vieta1  24408  aaliou3lem5  24443  aaliou3lem6  24444  aaliou3lem7  24445  taylpfval  24460  pserdvlem2  24523  abelthlem6  24531  logfac  24688  advlogexp  24742  emcllem2  25075  emcllem3  25076  emcllem7  25080  harmonicbnd  25082  harmonicbnd2  25083  harmonicbnd3  25086  harmonicbnd4  25089  chtval  25188  chpval  25200  chtfl  25227  chpfl  25228  chtprm  25231  chtnprm  25232  chpp1  25233  chtdif  25236  prmorcht  25256  musum  25269  muinv  25271  logfaclbnd  25299  logfacbnd3  25300  logexprlim  25302  chtppilimlem1  25514  rplogsumlem2  25526  rpvmasumlem  25528  dchrisumlem1  25530  dchrisumlem2  25531  dchrisumlem3  25532  dchrisum  25533  dchrisum0fval  25546  dchrisum0ff  25548  dchrisum0flblem1  25549  dchrisum0lem2  25559  dchrisum0  25561  mulog2sumlem1  25575  2vmadivsumlem  25581  log2sumbnd  25585  logdivbnd  25597  selberg3lem1  25598  pntrsumbnd  25607  pntrsumbnd2  25608  pntrlog2bndlem1  25618  pntrlog2bndlem4  25621  pntpbnd1  25627  pntpbnd2  25628  pntlemf  25646  brcgr  26137  axlowdimlem16  26194  eengv  26216  finsumvtxdg2sstep  26799  eulerpartlemgs2  30958  signsvfn  31179  fsum2dsub  31205  reprval  31208  reprsuc  31213  hashrepr  31223  chpvalz  31226  chtvalz  31227  breprexplema  31228  breprexplemc  31230  breprexp  31231  breprexpnat  31232  vtsval  31235  circlemeth  31238  hgt750lemb  31254  hgt750lema  31255  tgoldbachgtda  31259  tgoldbachgt  31261  subfacval2  31686  subfaclim  31687  bccolsum  32139  knoppndvlem6  33016  mettrifi  34040  rrncmslem  34118  k0004val  39226  binomcxplemnn0  39326  fsumnncl  40543  fsumsplit1  40544  fsumiunss  40547  fsumsermpt  40551  sumnnodd  40602  dvnmul  40898  dvnprodlem3  40903  itgspltprt  40934  stoweidlem17  40973  stoweidlem20  40976  stirlinglem12  41041  dirkertrigeqlem1  41054  dirkertrigeqlem3  41056  fourierdlem83  41145  fourierdlem112  41174  fourierdlem113  41175  elaa2lem  41189  etransclem32  41222  sge00  41332  sge0iunmptlemre  41371  sge0reuzb  41404  meaiuninclem  41436  carageniuncllem1  41477  hoidmvlelem3  41553  pwdif  42279  nnsum3primes4  42454  nnsum3primesprm  42456  nnsum3primesgbe  42458  nnsum4primesodd  42462  nnsum4primesoddALTV  42463  wtgoldbnnsum4prm  42468  bgoldbnnsum3prm  42470  altgsumbcALT  42926  nn0sumshdiglemA  43208  nn0sumshdiglemB  43209  nn0sumshdiglem1  43210  nn0sumshdiglem2  43211
  Copyright terms: Public domain W3C validator