Theorem sumeq2dv 15675

Description: Equality deduction for sum. (Contributed by NM, 3-Jan-2006.) (Revised by Mario Carneiro, 31-Jan-2014.)

Hypothesis

Ref	Expression
sumeq2dv.1	⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 = 𝐶)

Assertion

Ref	Expression
sumeq2dv	⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶)

Distinct variable groups:   𝐴,𝑘   𝜑,𝑘

Allowed substitution hints:   𝐵(𝑘)   𝐶(𝑘)

Proof of Theorem sumeq2dv

Step	Hyp	Ref	Expression
1		sumeq2dv.1	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 = 𝐶)
2	1	ralrimiva 3126	. 2 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 = 𝐶)
3	2	sumeq2d 15674	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Σcsu 15659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-om 7846  df-1st 7971  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221  df-sub 11414  df-neg 11415  df-nn 12194  df-n0 12450  df-z 12537  df-uz 12801  df-fz 13476  df-seq 13974  df-sum 15660

This theorem is referenced by:  2sumeq2dv  15678  sumeq12dv  15679  sumeq12rdv  15680  fsumf1o  15696  fsumss  15698  fsumsplit  15714  isummulc1  15736  isumdivc  15737  isumge0  15739  fsum2dlem  15743  fsumshftm  15754  fsum0diag2  15756  fsummulc1  15758  fsumdivc  15759  fsumneg  15760  fsumsub  15761  fsum2mul  15762  telfsumo2  15776  fsumparts  15779  hashiun  15795  hash2iun  15796  hash2iun1dif1  15797  ackbijnn  15801  binomlem  15802  binom1p  15804  incexclem  15809  incexc  15810  incexc2  15811  isum1p  15814  arisum  15833  trireciplem  15835  geoserg  15839  pwdif  15841  geo2sum  15846  mertenslem1  15857  mertenslem2  15858  mertens  15859  binomfallfaclem2  16013  binomrisefac  16015  bpolylem  16021  bpolydiflem  16027  fsumkthpow  16029  efaddlem  16066  rpnnen2lem10  16198  rpnnen2lem11  16199  fsumdvds  16285  pwp1fsum  16368  phisum  16768  pcfac  16877  ramcl  17007  lagsubg2  19133  sylow2a  19556  rrxcph  25299  trirn  25307  rrxmval  25312  rrxmet  25315  ovoliunnul  25415  ovolicc2lem4  25428  uniioombllem4  25494  vitalilem5  25520  itg1addlem4  25607  itg1addlem5  25608  itg1mulc  25612  itg10a  25618  itg1climres  25622  itgss  25720  itgeqa  25722  itgsplit  25744  elply2  26108  elplyd  26114  plyeq0lem  26122  plyaddlem1  26125  plymullem1  26126  coeeulem  26136  coeeq2  26154  coemullem  26162  coe1termlem  26170  plycjlem  26189  plyrecj  26194  dvply1  26198  elqaalem3  26236  aareccl  26241  aannenlem1  26243  taylpval  26281  dvtaylp  26285  pserdvlem2  26345  pserdv2  26347  abelthlem8  26356  abelthlem9  26357  abelth  26358  logtayl  26576  leibpi  26859  birthdaylem2  26869  amgmlem  26907  emcllem5  26917  fsumharmonic  26929  lgamcvg2  26972  ftalem5  26994  basellem3  27000  basellem8  27005  sgmval2  27060  fsumdvdscom  27102  dvdsflsumcom  27105  musum  27108  musumsum  27109  muinv  27110  fsumdvdsmul  27112  fsumdvdsmulOLD  27114  sgmppw  27115  1sgmprm  27117  chtlepsi  27124  pclogsum  27133  vmasum  27134  logfac2  27135  chpval2  27136  chpchtsum  27137  logexprlim  27143  logfacrlim2  27144  perfectlem2  27148  dchrsum2  27186  sumdchr2  27188  dchrhash  27189  dchr2sum  27191  sum2dchr  27192  pcbcctr  27194  bposlem2  27203  lgsquadlem1  27298  lgsquadlem2  27299  chebbnd1lem1  27387  rplogsumlem1  27402  rplogsumlem2  27403  rpvmasumlem  27405  dchrisumlem1  27407  dchrisumlem2  27408  dchrmusum2  27412  dchrvmasumlem1  27413  dchrvmasum2lem  27414  dchrvmasum2if  27415  dchrvmasumiflem1  27419  dchrvmasumiflem2  27420  dchrisum0flblem1  27426  dchrisum0fno1  27429  rpvmasum2  27430  dchrisum0lem2a  27435  dchrisum0lem2  27436  dchrisum0lem3  27437  dchrisum0  27438  rplogsum  27445  mudivsum  27448  mulogsumlem  27449  mulogsum  27450  mulog2sumlem1  27452  mulog2sumlem2  27453  mulog2sumlem3  27454  vmalogdivsum2  27456  vmalogdivsum  27457  2vmadivsumlem  27458  logsqvma  27460  logsqvma2  27461  selberglem1  27463  selberglem2  27464  selberg  27466  selberg2  27469  selberg3lem1  27475  selberg4lem1  27478  selberg4  27479  pntrsumo1  27483  selbergr  27486  selberg3r  27487  selberg4r  27488  selberg34r  27489  pntsval2  27494  pntrlog2bndlem4  27498  pntrlog2bndlem5  27499  pntpbnd1  27504  pntlemk  27524  pntlemo  27525  axcgrrflx  28848  axcgrid  28850  axsegconlem1  28851  axsegconlem9  28859  ax5seglem1  28862  ax5seglem2  28863  ax5seglem9  28871  axlowdimlem16  28891  axlowdimlem17  28892  ecgrtg  28917  finsumvtxdg2ssteplem3  29482  rusgrnumwwlks  29911  fusgrhashclwwlkn  30015  fusgreghash2wsp  30274  numclwwlk6  30326  indsum  32791  indsumin  32792  elrgspnlem2  33201  eulerpartlemsv1  34354  eulerpartlemsf  34357  eulerpartlemgs2  34378  eulerpartlemn  34379  plymulx0  34545  signsvfn  34580  fsum2dsub  34605  reprsuc  34613  hashreprin  34618  reprpmtf1o  34624  breprexplema  34628  breprexplemc  34630  breprexp  34631  breprexpnat  34632  vtsprod  34637  circlemeth  34638  circlemethnat  34639  circlevma  34640  circlemethhgt  34641  hgt750lemd  34646  hgt750lemb  34654  hgt750lema  34655  subfaclim  35182  fwddifnp1  36160  knoppndvlem6  36512  rrnmet  37830  3factsumint2  42017  3factsumint3  42018  lcmineqlem1  42024  lcmineqlem3  42026  lcmineqlem6  42029  sticksstones8  42148  sticksstones9  42149  sticksstones10  42150  sticksstones11  42151  sticksstones12a  42152  sticksstones12  42153  sticksstones17  42158  sticksstones18  42159  sticksstones19  42160  aks6d1c6lem1  42165  aks6d1c6lem3  42167  aks6d1c7lem3  42177  unitscyglem2  42191  sumcubes  42308  fltnltalem  42657  jm2.22  42991  jm2.23  42992  flcidc  43166  binomcxplemnn0  44345  binomcxplemdvsum  44351  binomcxplemnotnn0  44352  mccllem  45602  isumneg  45607  sumnnodd  45635  dvnmul  45948  dvnprodlem2  45952  dvnprodlem3  45953  stoweidlem37  46042  dirkertrigeqlem2  46104  dirkertrigeqlem3  46105  fourierdlem81  46192  fourierdlem83  46194  fourierdlem93  46204  fourierdlem103  46214  fourierdlem104  46215  elaa2lem  46238  etransclem23  46262  etransclem24  46263  etransclem31  46270  etransclem32  46271  etransclem35  46274  etransclem46  46285  rrxtopnfi  46292  rrndistlt  46295  sge0z  46380  sge0fsummpt  46395  sge0sup  46396  sge0resplit  46411  sge0split  46414  sge0ltfirpmpt2  46431  omeiunltfirp  46524  carageniuncllem2  46527  hoidmvlelem2  46601  hoidmvlelem3  46602  perfectALTVlem2  47727  nnsum3primesprm  47795  nnsum3primesgbe  47797  nnsum4primeseven  47805  altgsumbc  48344  altgsumbcALT  48345  nn0sumshdiglemA  48612  nn0sumshdiglemB  48613  nn0sumshdig  48616  aacllem  49794  amgmwlem  49795