Theorem sumeq1d 11509

Description: Equality deduction for sum. (Contributed by NM, 1-Nov-2005.)

Hypothesis

Ref	Expression
sumeq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
sumeq1d	|- ( ph -> sum_ k e. A C = sum_ k e. B C )

Distinct variable groups:   A, k   B, k

Allowed substitution hints:   ph( k)   C( k)

Proof of Theorem sumeq1d

Step	Hyp	Ref	Expression
1		sumeq1d.1	. 2 |- ( ph -> A = B )
2		sumeq1 11498	. 2 |- ( A = B -> sum_ k e. A C = sum_ k e. B C )
3	1, 2	syl 14	1 |- ( ph -> sum_ k e. A C = sum_ k e. B C )

Syntax hints:   -> wi 4   = wceq 1364   sum_csu 11496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-dc 836  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-v 2762  df-un 3157  df-in 3159  df-ss 3166  df-if 3558  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-opab 4091  df-mpt 4092  df-cnv 4667  df-dm 4669  df-rn 4670  df-res 4671  df-iota 5215  df-f 5258  df-f1 5259  df-fo 5260  df-f1o 5261  df-fv 5262  df-ov 5921  df-oprab 5922  df-mpo 5923  df-recs 6358  df-frec 6444  df-seqfrec 10519  df-sumdc 11497

This theorem is referenced by:  sumeq12dv  11515  sumeq12rdv  11516  fsumf1o  11533  fisumss  11535  fsumcllem  11542  fsum1  11555  fzosump1  11560  fsump1  11563  fsum2d  11578  fisumcom2  11581  fsumshftm  11588  fisumrev2  11589  telfsumo  11609  telfsum  11611  telfsum2  11612  fsumparts  11613  fsumiun  11620  bcxmas  11632  isumsplit  11634  isum1p  11635  arisum  11641  arisum2  11642  geoserap  11650  geolim  11654  geo2sum2  11658  cvgratnnlemseq  11669  cvgratnnlemsumlt  11671  mertenslemub  11677  mertenslemi1  11678  mertenslem2  11679  mertensabs  11680  efcvgfsum  11810  eftlub  11833  effsumlt  11835  eirraplem  11920  pcfac  12488  gsumfzfsumlem0  14074  gsumfzfsumlemm  14075  elplyr  14886  cvgcmp2nlemabs  15522  trilpolemeq1  15530  nconstwlpolemgt0  15554