Theorem cbvsumi 15390

Description: Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.)

Hypotheses

Ref	Expression
cbvsumi.1	⊢ Ⅎ𝑘𝐵
cbvsumi.2	⊢ Ⅎ𝑗𝐶
cbvsumi.3	⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶)

Assertion

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

Distinct variable group:   𝑗,𝑘,𝐴

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

Proof of Theorem cbvsumi

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

Syntax hints:   → wi 4   = wceq 1541  Ⅎwnfc 2888  Σcsu 15378

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-11 2157  ax-12 2174  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-sbc 3720  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-opab 5141  df-mpt 5162  df-xp 5594  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-pred 6199  df-iota 6388  df-fv 6438  df-ov 7271  df-oprab 7272  df-mpo 7273  df-frecs 8081  df-wrecs 8112  df-recs 8186  df-rdg 8225  df-seq 13703  df-sum 15379

This theorem is referenced by:  sumfc  15402  sumss2  15419  fsumzcl2  15432  fsumsplitf  15435  sumsnf  15436  sumsns  15443  fsummsnunz  15447  fsumsplitsnun  15448  fsum2dlem  15463  fsumcom2  15467  fsumshftm  15474  fsumrlim  15504  fsumo1  15505  o1fsum  15506  fsumiun  15514  ovolfiniun  24646  ovoliun2  24651  volfiniun  24692  itgfsum  24972  elplyd  25344  coeeq2  25384  fsumdvdscom  26315  fsumdvdsmul  26325  fsumvma  26342  fsumshftd  36945  binomcxplemdvsum  41926  sumsnd  42522  fourierdlem115  43716  fsummsndifre  44776  fsumsplitsndif  44777  fsummmodsndifre  44778  fsummmodsnunz  44779