Theorem sumeq2dv 15718

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 3132	. 2 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 = 𝐶)
3	2	sumeq2d 15717	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶)

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

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729  ax-cnex 11185  ax-resscn 11186  ax-1cn 11187  ax-icn 11188  ax-addcl 11189  ax-addrcl 11190  ax-mulcl 11191  ax-mulrcl 11192  ax-mulcom 11193  ax-addass 11194  ax-mulass 11195  ax-distr 11196  ax-i2m1 11197  ax-1ne0 11198  ax-1rid 11199  ax-rnegex 11200  ax-rrecex 11201  ax-cnre 11202  ax-pre-lttri 11203  ax-pre-lttrn 11204  ax-pre-ltadd 11205  ax-pre-mulgt0 11206

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-riota 7362  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7862  df-1st 7988  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-er 8719  df-en 8960  df-dom 8961  df-sdom 8962  df-pnf 11271  df-mnf 11272  df-xr 11273  df-ltxr 11274  df-le 11275  df-sub 11468  df-neg 11469  df-nn 12241  df-n0 12502  df-z 12589  df-uz 12853  df-fz 13525  df-seq 14020  df-sum 15703

This theorem is referenced by:  2sumeq2dv  15721  sumeq12dv  15722  sumeq12rdv  15723  fsumf1o  15739  fsumss  15741  fsumsplit  15757  isummulc1  15779  isumdivc  15780  isumge0  15782  fsum2dlem  15786  fsumshftm  15797  fsum0diag2  15799  fsummulc1  15801  fsumdivc  15802  fsumneg  15803  fsumsub  15804  fsum2mul  15805  telfsumo2  15819  fsumparts  15822  hashiun  15838  hash2iun  15839  hash2iun1dif1  15840  ackbijnn  15844  binomlem  15845  binom1p  15847  incexclem  15852  incexc  15853  incexc2  15854  isum1p  15857  arisum  15876  trireciplem  15878  geoserg  15882  pwdif  15884  geo2sum  15889  mertenslem1  15900  mertenslem2  15901  mertens  15902  binomfallfaclem2  16056  binomrisefac  16058  bpolylem  16064  bpolydiflem  16070  fsumkthpow  16072  efaddlem  16109  rpnnen2lem10  16241  rpnnen2lem11  16242  fsumdvds  16327  pwp1fsum  16410  phisum  16810  pcfac  16919  ramcl  17049  lagsubg2  19177  sylow2a  19600  rrxcph  25344  trirn  25352  rrxmval  25357  rrxmet  25360  ovoliunnul  25460  ovolicc2lem4  25473  uniioombllem4  25539  vitalilem5  25565  itg1addlem4  25652  itg1addlem5  25653  itg1mulc  25657  itg10a  25663  itg1climres  25667  itgss  25765  itgeqa  25767  itgsplit  25789  elply2  26153  elplyd  26159  plyeq0lem  26167  plyaddlem1  26170  plymullem1  26171  coeeulem  26181  coeeq2  26199  coemullem  26207  coe1termlem  26215  plycjlem  26234  plyrecj  26239  dvply1  26243  elqaalem3  26281  aareccl  26286  aannenlem1  26288  taylpval  26326  dvtaylp  26330  pserdvlem2  26390  pserdv2  26392  abelthlem8  26401  abelthlem9  26402  abelth  26403  logtayl  26621  leibpi  26904  birthdaylem2  26914  amgmlem  26952  emcllem5  26962  fsumharmonic  26974  lgamcvg2  27017  ftalem5  27039  basellem3  27045  basellem8  27050  sgmval2  27105  fsumdvdscom  27147  dvdsflsumcom  27150  musum  27153  musumsum  27154  muinv  27155  fsumdvdsmul  27157  fsumdvdsmulOLD  27159  sgmppw  27160  1sgmprm  27162  chtlepsi  27169  pclogsum  27178  vmasum  27179  logfac2  27180  chpval2  27181  chpchtsum  27182  logexprlim  27188  logfacrlim2  27189  perfectlem2  27193  dchrsum2  27231  sumdchr2  27233  dchrhash  27234  dchr2sum  27236  sum2dchr  27237  pcbcctr  27239  bposlem2  27248  lgsquadlem1  27343  lgsquadlem2  27344  chebbnd1lem1  27432  rplogsumlem1  27447  rplogsumlem2  27448  rpvmasumlem  27450  dchrisumlem1  27452  dchrisumlem2  27453  dchrmusum2  27457  dchrvmasumlem1  27458  dchrvmasum2lem  27459  dchrvmasum2if  27460  dchrvmasumiflem1  27464  dchrvmasumiflem2  27465  dchrisum0flblem1  27471  dchrisum0fno1  27474  rpvmasum2  27475  dchrisum0lem2a  27480  dchrisum0lem2  27481  dchrisum0lem3  27482  dchrisum0  27483  rplogsum  27490  mudivsum  27493  mulogsumlem  27494  mulogsum  27495  mulog2sumlem1  27497  mulog2sumlem2  27498  mulog2sumlem3  27499  vmalogdivsum2  27501  vmalogdivsum  27502  2vmadivsumlem  27503  logsqvma  27505  logsqvma2  27506  selberglem1  27508  selberglem2  27509  selberg  27511  selberg2  27514  selberg3lem1  27520  selberg4lem1  27523  selberg4  27524  pntrsumo1  27528  selbergr  27531  selberg3r  27532  selberg4r  27533  selberg34r  27534  pntsval2  27539  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  pntpbnd1  27549  pntlemk  27569  pntlemo  27570  axcgrrflx  28893  axcgrid  28895  axsegconlem1  28896  axsegconlem9  28904  ax5seglem1  28907  ax5seglem2  28908  ax5seglem9  28916  axlowdimlem16  28936  axlowdimlem17  28937  ecgrtg  28962  finsumvtxdg2ssteplem3  29527  rusgrnumwwlks  29956  fusgrhashclwwlkn  30060  fusgreghash2wsp  30319  numclwwlk6  30371  indsum  32838  indsumin  32839  elrgspnlem2  33238  eulerpartlemsv1  34388  eulerpartlemsf  34391  eulerpartlemgs2  34412  eulerpartlemn  34413  plymulx0  34579  signsvfn  34614  fsum2dsub  34639  reprsuc  34647  hashreprin  34652  reprpmtf1o  34658  breprexplema  34662  breprexplemc  34664  breprexp  34665  breprexpnat  34666  vtsprod  34671  circlemeth  34672  circlemethnat  34673  circlevma  34674  circlemethhgt  34675  hgt750lemd  34680  hgt750lemb  34688  hgt750lema  34689  subfaclim  35210  fwddifnp1  36183  knoppndvlem6  36535  rrnmet  37853  3factsumint2  42035  3factsumint3  42036  lcmineqlem1  42042  lcmineqlem3  42044  lcmineqlem6  42047  sticksstones8  42166  sticksstones9  42167  sticksstones10  42168  sticksstones11  42169  sticksstones12a  42170  sticksstones12  42171  sticksstones17  42176  sticksstones18  42177  sticksstones19  42178  aks6d1c6lem1  42183  aks6d1c6lem3  42185  aks6d1c7lem3  42195  unitscyglem2  42209  sumcubes  42362  fltnltalem  42685  jm2.22  43019  jm2.23  43020  flcidc  43194  binomcxplemnn0  44373  binomcxplemdvsum  44379  binomcxplemnotnn0  44380  mccllem  45626  isumneg  45631  sumnnodd  45659  dvnmul  45972  dvnprodlem2  45976  dvnprodlem3  45977  stoweidlem37  46066  dirkertrigeqlem2  46128  dirkertrigeqlem3  46129  fourierdlem81  46216  fourierdlem83  46218  fourierdlem93  46228  fourierdlem103  46238  fourierdlem104  46239  elaa2lem  46262  etransclem23  46286  etransclem24  46287  etransclem31  46294  etransclem32  46295  etransclem35  46298  etransclem46  46309  rrxtopnfi  46316  rrndistlt  46319  sge0z  46404  sge0fsummpt  46419  sge0sup  46420  sge0resplit  46435  sge0split  46438  sge0ltfirpmpt2  46455  omeiunltfirp  46548  carageniuncllem2  46551  hoidmvlelem2  46625  hoidmvlelem3  46626  perfectALTVlem2  47736  nnsum3primesprm  47804  nnsum3primesgbe  47806  nnsum4primeseven  47814  altgsumbc  48327  altgsumbcALT  48328  nn0sumshdiglemA  48599  nn0sumshdiglemB  48600  nn0sumshdig  48603  aacllem  49665  amgmwlem  49666