Theorem sumeq2dv 15881

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2146  Σcsu 15865

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5251  ax-nul 5262  ax-pow 5330  ax-pr 5394  ax-un 7758  ax-cnex 11266  ax-resscn 11267  ax-1cn 11268  ax-icn 11269  ax-addcl 11270  ax-addrcl 11271  ax-mulcl 11272  ax-mulrcl 11273  ax-mulcom 11274  ax-addass 11275  ax-mulass 11276  ax-distr 11277  ax-i2m1 11278  ax-1ne0 11279  ax-1rid 11280  ax-rnegex 11281  ax-rrecex 11282  ax-cnre 11283  ax-pre-lttri 11284  ax-pre-lttrn 11285  ax-pre-ltadd 11286  ax-pre-mulgt0 11287

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3369  df-rab 3416  df-v 3455  df-sbc 3742  df-csb 3851  df-ss 3900  df-pss 4016  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-pw 4561  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-iun 4955  df-br 5106  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5549  df-eprel 5554  df-po 5562  df-so 5563  df-fr 5607  df-we 5609  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 6310  df-ord 6371  df-on 6372  df-lim 6373  df-suc 6374  df-iota 6500  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-riota 7384  df-ov 7430  df-oprab 7431  df-mpo 7432  df-om 7885  df-1st 8008  df-2nd 8009  df-frecs 8310  df-wrecs 8341  df-recs 8390  df-rdg 8429  df-er 8728  df-en 8985  df-dom 8986  df-sdom 8987  df-pnf 11355  df-mnf 11356  df-xr 11357  df-ltxr 11358  df-le 11359  df-sub 11553  df-neg 11554  df-nn 12346  df-n0 12617  df-z 12704  df-uz 12976  df-fz 13650  df-seq 14155  df-sum 15866

This theorem is used by:  2sumeq2dv  15883  sumeq12dv  15884  sumeq12rdv  15885  fsumf1o  15901  fsumss  15903  fsumsplit  15919  isummulc1  15941  isumdivc  15942  isumge0  15944  fsum2dlem  15948  fsumshftm  15959  fsum0diag2  15961  fsummulc1  15963  fsumdivc  15964  fsumneg  15965  fsumsub  15966  fsum2mul  15967  telfsumo2  15982  fsumparts  15985  hashiun  16001  hash2iun  16002  hash2iun1dif1  16003  indsum  16007  ackbijnn  16009  binomlem  16010  binom1p  16012  incexclem  16017  incexc  16018  incexc2  16019  isum1p  16022  arisum  16041  trireciplem  16043  geoserg  16047  pwdif  16049  geo2sum  16054  mertenslem1  16065  mertenslem2  16066  mertens  16067  binomfallfaclem2  16218  binomrisefac  16220  bpolylem  16226  bpolydiflem  16232  fsumkthpow  16234  efaddlem  16271  rpnnen2lem10  16403  rpnnen2lem11  16404  fsumdvds  16490  pwp1fsum  16573  phisum  16980  pcfac  17089  ramcl  17219  lagsubg2  19421  sylow2a  19845  rrxcph  25725  trirn  25733  rrxmval  25738  rrxmet  25741  ovoliunnul  25840  ovolicc2lem4  25853  uniioombllem4  25919  vitalilem5  25945  itg1addlem4  26032  itg1addlem5  26033  itg1mulc  26037  itg10a  26043  itg1climres  26047  itgss  26144  itgeqa  26146  itgsplit  26168  elply2  26526  elplyd  26532  plyeq0lem  26541  plyaddlem1  26544  plymullem1  26545  coeeulem  26555  coeeq2  26573  coemullem  26581  coe1termlem  26589  plycjlem  26607  plyrecj  26610  plyn0mulidp  26614  dvply1  26617  elqaalem3  26656  aareccl  26665  aannenlem1  26667  taylpval  26706  dvtaylp  26709  pserdvlem2  26767  pserdv2  26769  abelthlem8  26778  abelthlem9  26779  abelth  26780  logtayl  27000  leibpi  27282  birthdaylem2  27292  amgmlem  27329  emcllem5  27339  fsumharmonic  27351  lgamcvg2  27394  ftalem5  27416  basellem3  27422  basellem8  27427  sgmval2  27482  fsumdvdscom  27524  dvdsflsumcom  27527  musum  27530  musumsum  27531  muinv  27532  fsumdvdsmul  27534  sgmppw  27536  1sgmprm  27538  chtlepsi  27545  pclogsum  27554  vmasum  27555  logfac2  27556  chpval2  27557  chpchtsum  27558  logexprlim  27564  logfacrlim2  27565  perfectlem2  27569  dchrsum2  27607  sumdchr2  27609  dchrhash  27610  dchr2sum  27612  sum2dchr  27613  pcbcctr  27615  bposlem2  27624  lgsquadlem1  27719  lgsquadlem2  27720  chebbnd1lem1  27808  rplogsumlem1  27823  rplogsumlem2  27824  rpvmasumlem  27826  dchrisumlem1  27828  dchrisumlem2  27829  dchrmusum2  27833  dchrvmasumlem1  27834  dchrvmasum2lem  27835  dchrvmasum2if  27836  dchrvmasumiflem1  27840  dchrvmasumiflem2  27841  dchrisum0flblem1  27847  dchrisum0fno1  27850  rpvmasum2  27851  dchrisum0lem2a  27856  dchrisum0lem2  27857  dchrisum0lem3  27858  dchrisum0  27859  rplogsum  27866  mudivsum  27869  mulogsumlem  27870  mulogsum  27871  mulog2sumlem1  27873  mulog2sumlem2  27874  mulog2sumlem3  27875  vmalogdivsum2  27877  vmalogdivsum  27878  2vmadivsumlem  27879  logsqvma  27881  logsqvma2  27882  selberglem1  27884  selberglem2  27885  selberg  27887  selberg2  27890  selberg3lem1  27896  selberg4lem1  27899  selberg4  27900  pntrsumo1  27904  selbergr  27907  selberg3r  27908  selberg4r  27909  selberg34r  27910  pntsval2  27915  pntrlog2bndlem4  27919  pntrlog2bndlem5  27920  pntpbnd1  27925  pntlemk  27945  pntlemo  27946  axcgrrflx  29504  axcgrid  29506  axsegconlem1  29507  axsegconlem9  29515  ax5seglem1  29518  ax5seglem2  29519  ax5seglem9  29527  axlowdimlem16  29547  axlowdimlem17  29548  ecgrtg  29573  finsumvtxdg2ssteplem3  30140  rusgrnumwwlks  30578  fusgrhashclwwlkn  30682  fusgreghash2wsp  30951  numclwwlk6  31003  indsumin  33481  elrgspnlem2  33857  vietadeg1  34263  eulerpartlemsv1  35041  eulerpartlemsf  35044  eulerpartlemgs2  35065  eulerpartlemn  35066  signsvfn  35264  fsum2dsub  35289  reprsuc  35297  hashreprin  35302  reprpmtf1o  35308  breprexplema  35312  breprexplemc  35314  breprexp  35315  breprexpnat  35316  vtsprod  35321  circlemeth  35322  circlemethnat  35323  circlevma  35324  circlemethhgt  35325  hgt750lemd  35330  hgt750lemb  35338  hgt750lema  35339  subfaclim  36074  fwddifnp1  37057  knoppndvlem6  37510  rrnmet  38903  3factsumint2  43212  3factsumint3  43213  lcmineqlem1  43219  lcmineqlem3  43221  lcmineqlem6  43224  sticksstones8  43343  sticksstones9  43344  sticksstones10  43345  sticksstones11  43346  sticksstones12a  43347  sticksstones12  43348  sticksstones17  43353  sticksstones18  43354  sticksstones19  43355  aks6d1c6lem1  43360  aks6d1c6lem3  43362  aks6d1c7lem3  43372  unitscyglem2  43386  sumcubes  43510  fltnltalem  43813  jm2.22  44142  jm2.23  44143  flcidc  44312  binomcxplemnn0  45473  binomcxplemdvsum  45479  binomcxplemnotnn0  45480  mccllem  46748  isumneg  46753  sumnnodd  46781  dvnmul  47092  dvnprodlem2  47096  dvnprodlem3  47097  stoweidlem37  47186  dirkertrigeqlem2  47248  dirkertrigeqlem3  47249  fourierdlem81  47336  fourierdlem83  47338  fourierdlem93  47348  fourierdlem103  47358  fourierdlem104  47359  elaa2lem  47382  etransclem23  47406  etransclem24  47407  etransclem31  47414  etransclem32  47415  etransclem35  47418  etransclem46  47429  rrxtopnfi  47436  rrndistlt  47439  sge0z  47524  sge0fsummpt  47539  sge0sup  47540  sge0resplit  47555  sge0split  47558  sge0ltfirpmpt2  47575  omeiunltfirp  47668  carageniuncllem2  47671  hoidmvlelem2  47745  hoidmvlelem3  47746  ppivalnn  48856  perfectALTVlem2  48959  nnsum3primesprm  49027  nnsum3primesgbe  49029  nnsum4primeseven  49037  altgsumbc  49603  altgsumbcALT  49604  nn0sumshdiglemA  49870  nn0sumshdiglemB  49871  nn0sumshdig  49874  aacllem  51153  amgmwlem  51201