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

Theorem cbvsumi 13170
Description: Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.)
Hypotheses
Ref Expression
cbvsumi.1  |-  F/_ k B
cbvsumi.2  |-  F/_ j C
cbvsumi.3  |-  ( j  =  k  ->  B  =  C )
Assertion
Ref Expression
cbvsumi  |-  sum_ j  e.  A  B  =  sum_ k  e.  A  C
Distinct variable group:    j, k, A
Allowed substitution hints:    B( j, k)    C( j, k)

Proof of Theorem cbvsumi
StepHypRef Expression
1 cbvsumi.3 . 2  |-  ( j  =  k  ->  B  =  C )
2 nfcv 2577 . 2  |-  F/_ k A
3 nfcv 2577 . 2  |-  F/_ j A
4 cbvsumi.1 . 2  |-  F/_ k B
5 cbvsumi.2 . 2  |-  F/_ j C
61, 2, 3, 4, 5cbvsum 13168 1  |-  sum_ j  e.  A  B  =  sum_ k  e.  A  C
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1364   F/_wnfc 2564   sum_csu 13159
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-br 4290  df-opab 4348  df-mpt 4349  df-cnv 4844  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fv 5423  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-recs 6828  df-rdg 6862  df-seq 11803  df-sum 13160
This theorem is referenced by:  sumfc  13182  sumss2  13199  sumsn  13213  sumsns  13215  fsum2dlem  13233  fsumcom2  13237  fsumshftm  13244  fsumrlim  13270  fsumo1  13271  o1fsum  13272  fsumiun  13280  ovolfiniun  20943  ovoliun2  20948  volfiniun  20987  itgfsum  21263  elplyd  21629  coeeq2  21669  fsumdvdscom  22484  fsumdvdsmul  22494  fsumvma  22511  sumsnd  29673  fsumz  30161  fsummsndifre  30162  fsumsplitsndif  30163  fsummmodsndifre  30164  fsummsnunz  30166  fsumsplitsnun  30167  fsummmodsnunre  30168
  Copyright terms: Public domain W3C validator