Theorem sumeq2dv 15792

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  Σcsu 15776

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7737  ax-cnex 11183  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7371  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7864  df-1st 7987  df-2nd 7988  df-frecs 8281  df-wrecs 8312  df-recs 8361  df-rdg 8400  df-er 8699  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11470  df-neg 11471  df-nn 12261  df-n0 12532  df-z 12619  df-uz 12891  df-fz 13565  df-seq 14069  df-sum 15777

This theorem is used by:  2sumeq2dv  15794  sumeq12dv  15795  sumeq12rdv  15796  fsumf1o  15812  fsumss  15814  fsumsplit  15830  isummulc1  15852  isumdivc  15853  isumge0  15855  fsum2dlem  15859  fsumshftm  15870  fsum0diag2  15872  fsummulc1  15874  fsumdivc  15875  fsumneg  15876  fsumsub  15877  fsum2mul  15878  telfsumo2  15893  fsumparts  15896  hashiun  15912  hash2iun  15913  hash2iun1dif1  15914  indsum  15918  ackbijnn  15920  binomlem  15921  binom1p  15923  incexclem  15928  incexc  15929  incexc2  15930  isum1p  15933  arisum  15952  trireciplem  15954  geoserg  15958  pwdif  15960  geo2sum  15965  mertenslem1  15976  mertenslem2  15977  mertens  15978  binomfallfaclem2  16129  binomrisefac  16131  bpolylem  16137  bpolydiflem  16143  fsumkthpow  16145  efaddlem  16182  rpnnen2lem10  16314  rpnnen2lem11  16315  fsumdvds  16401  pwp1fsum  16484  phisum  16885  pcfac  16994  ramcl  17124  lagsubg2  19325  sylow2a  19749  rrxcph  25623  trirn  25631  rrxmval  25636  rrxmet  25639  ovoliunnul  25738  ovolicc2lem4  25751  uniioombllem4  25817  vitalilem5  25843  itg1addlem4  25930  itg1addlem5  25931  itg1mulc  25935  itg10a  25941  itg1climres  25945  itgss  26042  itgeqa  26044  itgsplit  26066  elply2  26424  elplyd  26430  plyeq0lem  26439  plyaddlem1  26442  plymullem1  26443  coeeulem  26453  coeeq2  26471  coemullem  26479  coe1termlem  26487  plycjlem  26505  plyrecj  26510  plyn0mulidp  26514  dvply1  26517  elqaalem3  26556  aareccl  26565  aannenlem1  26567  taylpval  26606  dvtaylp  26609  pserdvlem2  26667  pserdv2  26669  abelthlem8  26678  abelthlem9  26679  abelth  26680  logtayl  26900  leibpi  27182  birthdaylem2  27192  amgmlem  27229  emcllem5  27239  fsumharmonic  27251  lgamcvg2  27294  ftalem5  27316  basellem3  27322  basellem8  27327  sgmval2  27382  fsumdvdscom  27424  dvdsflsumcom  27427  musum  27430  musumsum  27431  muinv  27432  fsumdvdsmul  27434  sgmppw  27436  1sgmprm  27438  chtlepsi  27445  pclogsum  27454  vmasum  27455  logfac2  27456  chpval2  27457  chpchtsum  27458  logexprlim  27464  logfacrlim2  27465  perfectlem2  27469  dchrsum2  27507  sumdchr2  27509  dchrhash  27510  dchr2sum  27512  sum2dchr  27513  pcbcctr  27515  bposlem2  27524  lgsquadlem1  27619  lgsquadlem2  27620  chebbnd1lem1  27708  rplogsumlem1  27723  rplogsumlem2  27724  rpvmasumlem  27726  dchrisumlem1  27728  dchrisumlem2  27729  dchrmusum2  27733  dchrvmasumlem1  27734  dchrvmasum2lem  27735  dchrvmasum2if  27736  dchrvmasumiflem1  27740  dchrvmasumiflem2  27741  dchrisum0flblem1  27747  dchrisum0fno1  27750  rpvmasum2  27751  dchrisum0lem2a  27756  dchrisum0lem2  27757  dchrisum0lem3  27758  dchrisum0  27759  rplogsum  27766  mudivsum  27769  mulogsumlem  27770  mulogsum  27771  mulog2sumlem1  27773  mulog2sumlem2  27774  mulog2sumlem3  27775  vmalogdivsum2  27777  vmalogdivsum  27778  2vmadivsumlem  27779  logsqvma  27781  logsqvma2  27782  selberglem1  27784  selberglem2  27785  selberg  27787  selberg2  27790  selberg3lem1  27796  selberg4lem1  27799  selberg4  27800  pntrsumo1  27804  selbergr  27807  selberg3r  27808  selberg4r  27809  selberg34r  27810  pntsval2  27815  pntrlog2bndlem4  27819  pntrlog2bndlem5  27820  pntpbnd1  27825  pntlemk  27845  pntlemo  27846  axcgrrflx  29374  axcgrid  29376  axsegconlem1  29377  axsegconlem9  29385  ax5seglem1  29388  ax5seglem2  29389  ax5seglem9  29397  axlowdimlem16  29417  axlowdimlem17  29418  ecgrtg  29443  finsumvtxdg2ssteplem3  30010  rusgrnumwwlks  30448  fusgrhashclwwlkn  30552  fusgreghash2wsp  30821  numclwwlk6  30873  indsumin  33310  elrgspnlem2  33686  vietadeg1  34091  eulerpartlemsv1  34870  eulerpartlemsf  34873  eulerpartlemgs2  34894  eulerpartlemn  34895  signsvfn  35093  fsum2dsub  35118  reprsuc  35126  hashreprin  35131  reprpmtf1o  35137  breprexplema  35141  breprexplemc  35143  breprexp  35144  breprexpnat  35145  vtsprod  35150  circlemeth  35151  circlemethnat  35152  circlevma  35153  circlemethhgt  35154  hgt750lemd  35159  hgt750lemb  35167  hgt750lema  35168  subfaclim  35770  fwddifnp1  36748  knoppndvlem6  37217  rrnmet  38582  3factsumint2  42891  3factsumint3  42892  lcmineqlem1  42898  lcmineqlem3  42900  lcmineqlem6  42903  sticksstones8  43022  sticksstones9  43023  sticksstones10  43024  sticksstones11  43025  sticksstones12a  43026  sticksstones12  43027  sticksstones17  43032  sticksstones18  43033  sticksstones19  43034  aks6d1c6lem1  43039  aks6d1c6lem3  43041  aks6d1c7lem3  43051  unitscyglem2  43065  sumcubes  43191  fltnltalem  43511  jm2.22  43839  jm2.23  43840  flcidc  44014  binomcxplemnn0  45176  binomcxplemdvsum  45182  binomcxplemnotnn0  45183  mccllem  46430  isumneg  46435  sumnnodd  46463  dvnmul  46774  dvnprodlem2  46778  dvnprodlem3  46779  stoweidlem37  46868  dirkertrigeqlem2  46930  dirkertrigeqlem3  46931  fourierdlem81  47018  fourierdlem83  47020  fourierdlem93  47030  fourierdlem103  47040  fourierdlem104  47041  elaa2lem  47064  etransclem23  47088  etransclem24  47089  etransclem31  47096  etransclem32  47097  etransclem35  47100  etransclem46  47111  rrxtopnfi  47118  rrndistlt  47121  sge0z  47206  sge0fsummpt  47221  sge0sup  47222  sge0resplit  47237  sge0split  47240  sge0ltfirpmpt2  47257  omeiunltfirp  47350  carageniuncllem2  47353  hoidmvlelem2  47427  hoidmvlelem3  47428  ppivalnn  48538  perfectALTVlem2  48641  nnsum3primesprm  48709  nnsum3primesgbe  48711  nnsum4primeseven  48719  altgsumbc  49285  altgsumbcALT  49286  nn0sumshdiglemA  49552  nn0sumshdiglemB  49553  nn0sumshdig  49556  aacllem  50775  amgmwlem  50823