Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  cbvsum Unicode version

Theorem cbvsum 11239
 Description: Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
Hypotheses
Ref Expression
cbvsum.1
cbvsum.2
cbvsum.3
cbvsum.4
cbvsum.5
Assertion
Ref Expression
cbvsum

Proof of Theorem cbvsum
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cbvsum.4 . . . . . . . . . . 11
2 cbvsum.5 . . . . . . . . . . 11
3 cbvsum.1 . . . . . . . . . . 11
41, 2, 3cbvcsb 3036 . . . . . . . . . 10
5 ifeq1 3508 . . . . . . . . . 10
64, 5ax-mp 5 . . . . . . . . 9
76mpteq2i 4051 . . . . . . . 8
8 seqeq3 10331 . . . . . . . 8
97, 8ax-mp 5 . . . . . . 7
109breq1i 3972 . . . . . 6
11103anbi3i 1175 . . . . 5 DECID DECID
1211rexbii 2464 . . . 4 DECID DECID
131, 2, 3cbvcsb 3036 . . . . . . . . . . . 12
14 ifeq1 3508 . . . . . . . . . . . 12
1513, 14ax-mp 5 . . . . . . . . . . 11
1615mpteq2i 4051 . . . . . . . . . 10
17 seqeq3 10331 . . . . . . . . . 10
1816, 17ax-mp 5 . . . . . . . . 9
1918fveq1i 5466 . . . . . . . 8
2019eqeq2i 2168 . . . . . . 7
2120anbi2i 453 . . . . . 6
2221exbii 1585 . . . . 5
2322rexbii 2464 . . . 4
2412, 23orbi12i 754 . . 3 DECID DECID
2524iotabii 5154 . 2 DECID DECID
26 df-sumdc 11233 . 2 DECID
27 df-sumdc 11233 . 2 DECID
2825, 26, 273eqtr4i 2188 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wo 698  DECID wdc 820   w3a 963   wceq 1335  wex 1472   wcel 2128  wnfc 2286  wral 2435  wrex 2436  csb 3031   wss 3102  cif 3505   class class class wbr 3965   cmpt 4025  cio 5130  wf1o 5166  cfv 5167  (class class class)co 5818  cc0 7715  c1 7716   caddc 7718   cle 7896  cn 8816  cz 9150  cuz 9422  cfz 9894   cseq 10326   cli 11157  csu 11232 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-rab 2444  df-v 2714  df-sbc 2938  df-csb 3032  df-un 3106  df-in 3108  df-ss 3115  df-if 3506  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-br 3966  df-opab 4026  df-mpt 4027  df-cnv 4591  df-dm 4593  df-rn 4594  df-res 4595  df-iota 5132  df-fv 5175  df-ov 5821  df-oprab 5822  df-mpo 5823  df-recs 6246  df-frec 6332  df-seqfrec 10327  df-sumdc 11233 This theorem is referenced by:  cbvsumv  11240  cbvsumi  11241  fsumsplitf  11287
 Copyright terms: Public domain W3C validator