Theorem cbvsumi 15409

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 2907	. 2 ⊢ Ⅎ𝑘𝐴
3		nfcv 2907	. 2 ⊢ Ⅎ𝑗𝐴
4		cbvsumi.1	. 2 ⊢ Ⅎ𝑘𝐵
5		cbvsumi.2	. 2 ⊢ Ⅎ𝑗𝐶
6	1, 2, 3, 4, 5	cbvsum 15407	1 ⊢ Σ𝑗 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   = wceq 1539  Ⅎwnfc 2887  Σcsu 15397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-11 2154  ax-12 2171  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-xp 5595  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-iota 6391  df-fv 6441  df-ov 7278  df-oprab 7279  df-mpo 7280  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-seq 13722  df-sum 15398

This theorem is referenced by:  sumfc  15421  sumss2  15438  fsumzcl2  15451  fsumsplitf  15454  sumsnf  15455  sumsns  15462  fsummsnunz  15466  fsumsplitsnun  15467  fsum2dlem  15482  fsumcom2  15486  fsumshftm  15493  fsumrlim  15523  fsumo1  15524  o1fsum  15525  fsumiun  15533  ovolfiniun  24665  ovoliun2  24670  volfiniun  24711  itgfsum  24991  elplyd  25363  coeeq2  25403  fsumdvdscom  26334  fsumdvdsmul  26344  fsumvma  26361  fsumshftd  36966  binomcxplemdvsum  41973  sumsnd  42569  fourierdlem115  43762  fsummsndifre  44824  fsumsplitsndif  44825  fsummmodsndifre  44826  fsummmodsnunz  44827