Theorem cbvsumv 14804

Description: Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jul-2013.)

Hypothesis

Ref	Expression
cbvsum.1	⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶)

Assertion

Ref	Expression
cbvsumv	⊢ Σ𝑗 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶

Distinct variable groups:   𝑗,𝑘,𝐴   𝐵,𝑘   𝐶,𝑗

Allowed substitution hints:   𝐵(𝑗)   𝐶(𝑘)

Proof of Theorem cbvsumv

Step	Hyp	Ref	Expression
1		cbvsum.1	. 2 ⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶)
2		nfcv 2970	. 2 ⊢ Ⅎ𝑘𝐴
3		nfcv 2970	. 2 ⊢ Ⅎ𝑗𝐴
4		nfcv 2970	. 2 ⊢ Ⅎ𝑘𝐵
5		nfcv 2970	. 2 ⊢ Ⅎ𝑗𝐶
6	1, 2, 3, 4, 5	cbvsum 14803	1 ⊢ Σ𝑗 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   = wceq 1658  Σcsu 14794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-ral 3123  df-rex 3124  df-rab 3127  df-v 3417  df-sbc 3664  df-csb 3759  df-dif 3802  df-un 3804  df-in 3806  df-ss 3813  df-nul 4146  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4660  df-br 4875  df-opab 4937  df-mpt 4954  df-xp 5349  df-cnv 5351  df-dm 5353  df-rn 5354  df-res 5355  df-ima 5356  df-pred 5921  df-iota 6087  df-fv 6132  df-ov 6909  df-oprab 6910  df-mpt2 6911  df-wrecs 7673  df-recs 7735  df-rdg 7773  df-seq 13097  df-sum 14795

This theorem is referenced by:  isumge0  14873  telfsumo  14909  fsumparts  14913  binomlem  14936  incexclem  14943  mertenslem1  14990  mertens  14992  binomfallfaclem2  15144  bpolyval  15153  efaddlem  15196  pwp1fsum  15489  bitsinv2  15539  prmreclem6  15997  ovolicc2lem4  23687  uniioombllem6  23755  plymullem1  24370  plyadd  24373  plymul  24374  coeeu  24381  coeid  24394  dvply1  24439  vieta1  24467  aaliou3  24506  abelthlem8  24593  abelthlem9  24594  abelth  24595  logtayl  24806  ftalem2  25214  ftalem6  25218  dchrsum2  25407  sumdchr2  25409  dchrisumlem1  25592  dchrisum  25595  dchrisum0fval  25608  dchrisum0ff  25610  rpvmasum  25629  mulog2sumlem1  25637  2vmadivsumlem  25643  logsqvma  25645  logsqvma2  25646  selberg  25651  chpdifbndlem1  25656  selberg3lem1  25660  selberg4lem1  25663  pntsval  25675  pntsval2  25679  pntpbnd1  25689  pntlemo  25710  axsegconlem9  26225  hashunif  30110  eulerpartlems  30968  eulerpartlemgs2  30988  breprexplema  31258  breprexplemc  31260  breprexp  31261  hgt750lema  31285  fwddifnp1  32812  binomcxplemnotnn0  39396  mccl  40626  sumnnodd  40658  dvnprodlem1  40957  dvnprodlem3  40959  dvnprod  40960  fourierdlem73  41191  fourierdlem112  41230  fourierdlem113  41231  etransclem11  41257  etransclem32  41278  etransclem35  41281  etransc  41295  fsumlesge0  41386  meaiuninclem  41489  omeiunltfirp  41528  hoidmvlelem3  41606  pwdif  42332  altgsumbcALT  42979  nn0sumshdiglemA  43261  nn0sumshdiglemB  43262