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

Theorem sumeq2sdv 15588
Description: Equality deduction for sum. (Contributed by NM, 3-Jan-2006.) (Proof shortened by Glauco Siliprandi, 5-Apr-2020.)
Hypothesis
Ref Expression
sumeq2sdv.1 (𝜑𝐵 = 𝐶)
Assertion
Ref Expression
sumeq2sdv (𝜑 → Σ𝑘𝐴 𝐵 = Σ𝑘𝐴 𝐶)
Distinct variable groups:   𝐴,𝑘   𝜑,𝑘
Allowed substitution hints:   𝐵(𝑘)   𝐶(𝑘)

Proof of Theorem sumeq2sdv
StepHypRef Expression
1 sumeq2sdv.1 . . 3 (𝜑𝐵 = 𝐶)
21ralrimivw 3147 . 2 (𝜑 → ∀𝑘𝐴 𝐵 = 𝐶)
32sumeq2d 15586 1 (𝜑 → Σ𝑘𝐴 𝐵 = Σ𝑘𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  Σcsu 15569
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-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7671  ax-cnex 11106  ax-resscn 11107  ax-1cn 11108  ax-icn 11109  ax-addcl 11110  ax-addrcl 11111  ax-mulcl 11112  ax-mulrcl 11113  ax-mulcom 11114  ax-addass 11115  ax-mulass 11116  ax-distr 11117  ax-i2m1 11118  ax-1ne0 11119  ax-1rid 11120  ax-rnegex 11121  ax-rrecex 11122  ax-cnre 11123  ax-pre-lttri 11124  ax-pre-lttrn 11125  ax-pre-ltadd 11126  ax-pre-mulgt0 11127
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7312  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7802  df-1st 7920  df-2nd 7921  df-frecs 8211  df-wrecs 8242  df-recs 8316  df-rdg 8355  df-er 8647  df-en 8883  df-dom 8884  df-sdom 8885  df-pnf 11190  df-mnf 11191  df-xr 11192  df-ltxr 11193  df-le 11194  df-sub 11386  df-neg 11387  df-nn 12153  df-n0 12413  df-z 12499  df-uz 12763  df-fz 13424  df-seq 13906  df-sum 15570
This theorem is referenced by:  sumsplit  15652  fsumrlim  15695  hash2iun1dif1  15708  incexclem  15720  bpolylem  15930  bpolyval  15931  efval  15961  rpnnen2lem12  16106  pcfac  16770  ramcl  16900  cshwshashnsame  16975  fsumcn  24231  fsum2cn  24232  lebnumlem3  24324  rrxdsfival  24775  uniioombllem6  24950  itg1climres  25077  itgeq1f  25134  itgeq2  25140  dvmptfsum  25337  elplyr  25560  plyeq0lem  25569  plyadd  25576  plymul  25577  coeeu  25584  coelem  25585  coeeq  25586  coeidlem  25596  coeid  25597  coeid2  25598  plyco  25600  plycjlem  25635  aareccl  25684  taylply2  25725  pserdvlem2  25785  pserdv  25786  abelthlem6  25793  abelthlem9  25797  logtayl  26013  leibpi  26290  basellem3  26430  dchrvmasum2if  26843  dchrvmaeq0  26850  rpvmasum2  26858  dchrisum0re  26859  brcgr  27796  axsegcon  27823  dipfval  29591  ipval  29592  fsumiunle  31669  itgeq12dv  32866  eulerpartleme  32903  eulerpartlemr  32914  eulerpartlemn  32921  reprsum  33166  reprsuc  33168  reprpmtf1o  33179  vtsval  33190  iprodgam  34255  fwddifnval  34738  knoppndvlem6  34970  knoppf  34988  rrnmval  36277  fsumshftd  37404  fsumcnf  43207  mccl  43810  dvnmul  44155  dvmptfprod  44157  dvnprodlem1  44158  dvnprodlem3  44160  dvnprod  44161  stoweidlem17  44229  stoweidlem26  44238  stoweidlem30  44242  stoweidlem32  44244  dirkertrigeq  44313  dirkeritg  44314  fourierdlem83  44401  fourierdlem103  44421  etransclem11  44457  etransclem24  44470  etransclem26  44472  etransclem27  44473  etransclem28  44474  etransclem31  44477  etransclem35  44481  etransclem46  44492  etransclem47  44493  rrndistlt  44502  ioorrnopn  44517  sge0val  44578  hoiqssbllem2  44835  nnsum3primes4  45951  nnsum4primesodd  45959  nnsum4primesoddALTV  45960  nnsum4primesevenALTV  45964  nn0sumshdiglemB  46677  nn0sumshdiglem1  46678  aacllem  47219
  Copyright terms: Public domain W3C validator