Theorem sumeq1 13511

Description: Equality theorem for a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)

Assertion

Ref	Expression
sumeq1

Proof of Theorem sumeq1

Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sseq1 3524	. . . . . 6
2		simpl 457	. . . . . . . . . . 11
3	2	eleq2d 2527	. . . . . . . . . 10
4	3	ifbid 3963	. . . . . . . . 9
5	4	mpteq2dva 4538	. . . . . . . 8
6	5	seqeq3d 12115	. . . . . . 7
7	6	breq1d 4462	. . . . . 6
8	1, 7	anbi12d 710	. . . . 5
9	8	rexbidv 2968	. . . 4
10		f1oeq3 5814	. . . . . . 7
11	10	anbi1d 704	. . . . . 6
12	11	exbidv 1714	. . . . 5
13	12	rexbidv 2968	. . . 4
14	9, 13	orbi12d 709	. . 3
15	14	iotabidv 5577	. 2
16		df-sum 13509	. 2
17		df-sum 13509	. 2
18	15, 16, 17	3eqtr4g 2523	1

Syntax hints:  ->wi 4  \/wo 368  /\wa 369  =wceq 1395  E.wex 1612  e.wcel 1818  E.wrex 2808  [_csb 3434  C_wss 3475  ifcif 3941   class class class wbr 4452  e.cmpt 4510  iotacio 5554  -1-1-onto->wf1o 5592  `cfv 5593  (class class class)co 6296  0cc0 9513  1c1 9514  caddc 9516  cn 10561  cz 10889  cuz 11110  cfz 11701  seqcseq 12107  cli 13307  sum_csu 13508

This theorem is referenced by:  sumeq1i  13520  sumeq1d  13523  sumz  13544  fsumadd  13561  fsum2d  13586  fsumrev2  13597  fsummulc2  13599  fsumconst  13605  modfsummods  13607  modfsummod  13608  fsumabs  13615  fsumrelem  13621  fsumrlim  13625  fsumo1  13626  fsumiun  13635  bitsinv2  14093  bitsf1ocnv  14094  bitsinv  14098  prmreclem5  14438  gsumfsum  18484  fsumcn  21374  ovolfiniun  21912  volfiniun  21957  itgfsum  22233  dvmptfsum  22376  pntrsumbnd2  23752  esumpcvgval  28084  esumcvg  28092  rrnval  30323  mccl  31606  dvmptfprod  31742  dvnprodlem1  31743  dvnprodlem2  31744  dvnprodlem3  31745  dvnprod  31746

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-mpt 4512  df-cnv 5012  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-recs 7061  df-rdg 7095  df-seq 12108  df-sum 13509