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

Theorem sumeq1d 14228
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 14216 . 2 (𝐴 = 𝐵 → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶)
31, 2syl 17 1 (𝜑 → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  Σcsu 14213
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4368  df-br 4579  df-opab 4639  df-mpt 4640  df-xp 5034  df-cnv 5036  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-iota 5754  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-wrecs 7272  df-recs 7333  df-rdg 7371  df-seq 12622  df-sum 14214
This theorem is referenced by:  sumeq12dv  14233  sumeq12rdv  14234  fsumf1o  14250  sumss  14251  fsumcllem  14259  fsum1  14269  fzosump1  14274  fsump1  14278  fsum2d  14293  fsumcom2  14296  fsumcom2OLD  14297  fsumshftm  14304  fsumrev2  14305  telfsumo  14324  telfsum  14326  telfsum2  14327  fsumparts  14328  fsumiun  14343  bcxmas  14355  incexclem  14356  incexc2  14358  isumsplit  14360  isum1p  14361  arisum  14380  arisum2  14381  geoser  14387  geolim  14389  geo2sum2  14393  mertenslem1  14404  mertenslem2  14405  mertens  14406  bpolydiflem  14573  efcvgfsum  14604  fprodefsum  14613  eftlub  14627  effsumlt  14629  eirrlem  14720  pwp1fsum  14901  bitsinv1  14951  bitsinvp1  14958  pcfac  15390  prmreclem4  15410  prmreclem6  15412  ovoliunlem1  23022  uniioombllem3  23104  itg11  23209  dvfsumlem1  23538  dvfsumlem4  23541  dvfsum2  23546  elplyr  23706  coeeu  23730  coeeq  23732  plyco  23746  0dgrb  23751  dvply2g  23789  vieta1lem2  23815  vieta1  23816  aaliou3lem5  23851  aaliou3lem6  23852  aaliou3lem7  23853  taylpfval  23868  pserdvlem2  23931  abelthlem6  23939  logfac  24096  advlogexp  24146  emcllem2  24468  emcllem3  24469  emcllem7  24473  harmonicbnd  24475  harmonicbnd2  24476  harmonicbnd3  24479  harmonicbnd4  24482  chtval  24581  chpval  24593  chtfl  24620  chpfl  24621  chtprm  24624  chtnprm  24625  chpp1  24626  chtdif  24629  prmorcht  24649  musum  24662  muinv  24664  logfaclbnd  24692  logfacbnd3  24693  logexprlim  24695  chtppilimlem1  24907  rplogsumlem2  24919  rpvmasumlem  24921  dchrisumlem1  24923  dchrisumlem2  24924  dchrisumlem3  24925  dchrisum  24926  dchrisum0fval  24939  dchrisum0ff  24941  dchrisum0flblem1  24942  dchrisum0lem2  24952  dchrisum0  24954  mulog2sumlem1  24968  2vmadivsumlem  24974  log2sumbnd  24978  logdivbnd  24990  selberg3lem1  24991  pntrsumbnd  25000  pntrsumbnd2  25001  pntrlog2bndlem1  25011  pntrlog2bndlem4  25014  pntpbnd1  25020  pntpbnd2  25021  pntlemf  25039  brcgr  25526  axlowdimlem16  25583  eengv  25605  eulerpartlemgs2  29563  signsvfn  29779  subfacval2  30217  subfaclim  30218  bccolsum  30672  knoppndvlem6  31472  mettrifi  32517  rrncmslem  32595  k0004val  37262  binomcxplemnn0  37364  fsumnncl  38432  fsumsplit1  38433  fsumiunss  38436  fsumsermpt  38440  sumnnodd  38491  dvnmul  38627  dvnprodlem3  38632  itgspltprt  38665  stoweidlem17  38704  stoweidlem20  38707  stirlinglem12  38772  dirkertrigeqlem1  38785  dirkertrigeqlem3  38787  fourierdlem83  38876  fourierdlem112  38905  fourierdlem113  38906  elaa2lem  38920  etransclem32  38953  sge00  39063  sge0iunmptlemre  39102  sge0reuzb  39135  meaiuninclem  39167  carageniuncllem1  39205  hoidmvlelem3  39281  pwdif  39834  nnsum3primes4  39999  nnsum3primesprm  40001  nnsum3primesgbe  40003  nnsum4primesodd  40007  nnsum4primesoddALTV  40008  wtgoldbnnsum4prm  40013  bgoldbnnsum3prm  40015  altgsumbcALT  41916  nn0sumshdiglemA  42203  nn0sumshdiglemB  42204  nn0sumshdiglem1  42205  nn0sumshdiglem2  42206
  Copyright terms: Public domain W3C validator