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

Theorem sumeq1d 15046
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 15033 . 2 (𝐴 = 𝐵 → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶)
31, 2syl 17 1 (𝜑 → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  Σcsu 15030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  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 7148  df-oprab 7149  df-mpo 7150  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-seq 13358  df-sum 15031
This theorem is referenced by:  sumeq12dv  15051  sumeq12rdv  15052  fsumf1o  15068  sumss  15069  fsumcllem  15077  fsum1  15090  fzosump1  15095  fsump1  15099  fsum2d  15114  fsumcom2  15117  fsumshftm  15124  fsumrev2  15125  telfsumo  15145  telfsum  15147  telfsum2  15148  fsumparts  15149  fsumiun  15164  bcxmas  15178  incexclem  15179  incexc2  15181  isumsplit  15183  isum1p  15184  arisum  15203  arisum2  15204  geoser  15210  pwdif  15211  geolim  15214  geo2sum2  15218  mertenslem1  15228  mertenslem2  15229  mertens  15230  bpolydiflem  15396  efcvgfsum  15427  fprodefsum  15436  eftlub  15450  effsumlt  15452  eirrlem  15545  pwp1fsum  15730  bitsinv1  15779  bitsinvp1  15786  pcfac  16223  prmreclem4  16243  prmreclem6  16245  ovoliunlem1  24030  uniioombllem3  24113  itg11  24219  dvfsumlem1  24550  dvfsumlem4  24553  dvfsum2  24558  elplyr  24718  coeeu  24742  coeeq  24744  plyco  24758  0dgrb  24763  dvply2g  24801  vieta1lem2  24827  vieta1  24828  aaliou3lem5  24863  aaliou3lem6  24864  aaliou3lem7  24865  taylpfval  24880  pserdvlem2  24943  abelthlem6  24951  logfac  25111  advlogexp  25165  emcllem2  25501  emcllem3  25502  emcllem7  25506  harmonicbnd  25508  harmonicbnd2  25509  harmonicbnd3  25512  harmonicbnd4  25515  chtval  25614  chpval  25626  chtfl  25653  chpfl  25654  chtprm  25657  chtnprm  25658  chpp1  25659  chtdif  25662  prmorcht  25682  musum  25695  muinv  25697  logfaclbnd  25725  logfacbnd3  25726  logexprlim  25728  chtppilimlem1  25976  rplogsumlem2  25988  rpvmasumlem  25990  dchrisumlem1  25992  dchrisumlem2  25993  dchrisumlem3  25994  dchrisum  25995  dchrisum0fval  26008  dchrisum0ff  26010  dchrisum0flblem1  26011  dchrisum0lem2  26021  dchrisum0  26023  mulog2sumlem1  26037  2vmadivsumlem  26043  log2sumbnd  26047  logdivbnd  26059  selberg3lem1  26060  pntrsumbnd  26069  pntrsumbnd2  26070  pntrlog2bndlem1  26080  pntrlog2bndlem4  26083  pntpbnd1  26089  pntpbnd2  26090  pntlemf  26108  brcgr  26613  axlowdimlem16  26670  eengv  26692  finsumvtxdg2sstep  27258  eulerpartlemgs2  31537  signsvfn  31751  fsum2dsub  31777  reprval  31780  reprsuc  31785  hashrepr  31795  chpvalz  31798  chtvalz  31799  breprexplema  31800  breprexplemc  31802  breprexp  31803  breprexpnat  31804  vtsval  31807  circlemeth  31810  hgt750lemb  31826  hgt750lema  31827  tgoldbachgtda  31831  tgoldbachgt  31833  subfacval2  32331  subfaclim  32332  bccolsum  32868  knoppndvlem6  33753  mettrifi  34913  rrncmslem  34991  fzosumm1  39004  k0004val  40378  binomcxplemnn0  40558  fsumnncl  41728  fsumsplit1  41729  fsumiunss  41732  fsumsermpt  41736  sumnnodd  41787  dvnmul  42104  dvnprodlem3  42109  itgspltprt  42140  stoweidlem17  42179  stoweidlem20  42182  stirlinglem12  42247  dirkertrigeqlem1  42260  dirkertrigeqlem3  42262  fourierdlem83  42351  fourierdlem112  42380  fourierdlem113  42381  elaa2lem  42395  etransclem32  42428  sge00  42535  sge0iunmptlemre  42574  sge0reuzb  42607  meaiuninclem  42639  carageniuncllem1  42680  hoidmvlelem3  42756  nnsum3primes4  43830  nnsum3primesprm  43832  nnsum3primesgbe  43834  nnsum4primesodd  43838  nnsum4primesoddALTV  43839  wtgoldbnnsum4prm  43844  bgoldbnnsum3prm  43846  altgsumbcALT  44329  nn0sumshdiglemA  44607  nn0sumshdiglemB  44608  nn0sumshdiglem1  44609  nn0sumshdiglem2  44610
  Copyright terms: Public domain W3C validator