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

Theorem cbvsumi 14224
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
StepHypRef Expression
1 cbvsumi.3 . 2 (𝑗 = 𝑘𝐵 = 𝐶)
2 nfcv 2750 . 2 𝑘𝐴
3 nfcv 2750 . 2 𝑗𝐴
4 cbvsumi.1 . 2 𝑘𝐵
5 cbvsumi.2 . 2 𝑗𝐶
61, 2, 3, 4, 5cbvsum 14222 1 Σ𝑗𝐴 𝐵 = Σ𝑘𝐴 𝐶
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wnfc 2737  Σcsu 14213
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-mpt 4639  df-xp 5034  df-cnv 5036  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-iota 5754  df-fv 5798  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-wrecs 7272  df-recs 7333  df-rdg 7371  df-seq 12622  df-sum 14214
This theorem is referenced by:  sumfc  14236  sumss2  14253  fsumzcl2  14265  sumsn  14268  sumsns  14272  fsummsnunz  14276  fsumsplitsnun  14277  fsum2dlem  14292  fsumcom2  14296  fsumcom2OLD  14297  fsumshftm  14304  fsumrlim  14333  fsumo1  14334  o1fsum  14335  fsumiun  14343  ovolfiniun  23021  ovoliun2  23026  volfiniun  23067  itgfsum  23344  elplyd  23707  coeeq2  23747  fsumdvdscom  24656  fsumdvdsmul  24666  fsumvma  24683  fsumshftd  33079  fsumshftdOLD  33080  binomcxplemdvsum  37400  sumsnd  38032  fsumsplitf  38458  sumsnf  38460  fourierdlem115  38938  fsummsndifre  40241  fsumsplitsndif  40242  fsummmodsndifre  40243  fsummmodsnunz  40244
  Copyright terms: Public domain W3C validator