Theorem sumeq2dv 15869

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

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

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 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751  ax-cnex 11256  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276  ax-pre-mulgt0 11277

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  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 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-1st 8001  df-2nd 8002  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349  df-sub 11543  df-neg 11544  df-nn 12336  df-n0 12607  df-z 12694  df-uz 12966  df-fz 13640  df-seq 14145  df-sum 15854

This theorem is used by:  2sumeq2dv  15871  sumeq12dv  15872  sumeq12rdv  15873  fsumf1o  15889  fsumss  15891  fsumsplit  15907  isummulc1  15929  isumdivc  15930  isumge0  15932  fsum2dlem  15936  fsumshftm  15947  fsum0diag2  15949  fsummulc1  15951  fsumdivc  15952  fsumneg  15953  fsumsub  15954  fsum2mul  15955  telfsumo2  15970  fsumparts  15973  hashiun  15989  hash2iun  15990  hash2iun1dif1  15991  indsum  15995  ackbijnn  15997  binomlem  15998  binom1p  16000  incexclem  16005  incexc  16006  incexc2  16007  isum1p  16010  arisum  16029  trireciplem  16031  geoserg  16035  pwdif  16037  geo2sum  16042  mertenslem1  16053  mertenslem2  16054  mertens  16055  binomfallfaclem2  16206  binomrisefac  16208  bpolylem  16214  bpolydiflem  16220  fsumkthpow  16222  efaddlem  16259  rpnnen2lem10  16391  rpnnen2lem11  16392  fsumdvds  16478  pwp1fsum  16561  phisum  16968  pcfac  17077  ramcl  17207  lagsubg2  19409  sylow2a  19833  rrxcph  25713  trirn  25721  rrxmval  25726  rrxmet  25729  ovoliunnul  25828  ovolicc2lem4  25841  uniioombllem4  25907  vitalilem5  25933  itg1addlem4  26020  itg1addlem5  26021  itg1mulc  26025  itg10a  26031  itg1climres  26035  itgss  26132  itgeqa  26134  itgsplit  26156  elply2  26514  elplyd  26520  plyeq0lem  26529  plyaddlem1  26532  plymullem1  26533  coeeulem  26543  coeeq2  26561  coemullem  26569  coe1termlem  26577  plycjlem  26595  plyrecj  26598  plyn0mulidp  26602  dvply1  26605  elqaalem3  26644  aareccl  26653  aannenlem1  26655  taylpval  26694  dvtaylp  26697  pserdvlem2  26755  pserdv2  26757  abelthlem8  26766  abelthlem9  26767  abelth  26768  logtayl  26988  leibpi  27270  birthdaylem2  27280  amgmlem  27317  emcllem5  27327  fsumharmonic  27339  lgamcvg2  27382  ftalem5  27404  basellem3  27410  basellem8  27415  sgmval2  27470  fsumdvdscom  27512  dvdsflsumcom  27515  musum  27518  musumsum  27519  muinv  27520  fsumdvdsmul  27522  sgmppw  27524  1sgmprm  27526  chtlepsi  27533  pclogsum  27542  vmasum  27543  logfac2  27544  chpval2  27545  chpchtsum  27546  logexprlim  27552  logfacrlim2  27553  perfectlem2  27557  dchrsum2  27595  sumdchr2  27597  dchrhash  27598  dchr2sum  27600  sum2dchr  27601  pcbcctr  27603  bposlem2  27612  lgsquadlem1  27707  lgsquadlem2  27708  chebbnd1lem1  27796  rplogsumlem1  27811  rplogsumlem2  27812  rpvmasumlem  27814  dchrisumlem1  27816  dchrisumlem2  27817  dchrmusum2  27821  dchrvmasumlem1  27822  dchrvmasum2lem  27823  dchrvmasum2if  27824  dchrvmasumiflem1  27828  dchrvmasumiflem2  27829  dchrisum0flblem1  27835  dchrisum0fno1  27838  rpvmasum2  27839  dchrisum0lem2a  27844  dchrisum0lem2  27845  dchrisum0lem3  27846  dchrisum0  27847  rplogsum  27854  mudivsum  27857  mulogsumlem  27858  mulogsum  27859  mulog2sumlem1  27861  mulog2sumlem2  27862  mulog2sumlem3  27863  vmalogdivsum2  27865  vmalogdivsum  27866  2vmadivsumlem  27867  logsqvma  27869  logsqvma2  27870  selberglem1  27872  selberglem2  27873  selberg  27875  selberg2  27878  selberg3lem1  27884  selberg4lem1  27887  selberg4  27888  pntrsumo1  27892  selbergr  27895  selberg3r  27896  selberg4r  27897  selberg34r  27898  pntsval2  27903  pntrlog2bndlem4  27907  pntrlog2bndlem5  27908  pntpbnd1  27913  pntlemk  27933  pntlemo  27934  axcgrrflx  29492  axcgrid  29494  axsegconlem1  29495  axsegconlem9  29503  ax5seglem1  29506  ax5seglem2  29507  ax5seglem9  29515  axlowdimlem16  29535  axlowdimlem17  29536  ecgrtg  29561  finsumvtxdg2ssteplem3  30128  rusgrnumwwlks  30566  fusgrhashclwwlkn  30670  fusgreghash2wsp  30939  numclwwlk6  30991  indsumin  33428  elrgspnlem2  33804  vietadeg1  34210  eulerpartlemsv1  34988  eulerpartlemsf  34991  eulerpartlemgs2  35012  eulerpartlemn  35013  signsvfn  35211  fsum2dsub  35236  reprsuc  35244  hashreprin  35249  reprpmtf1o  35255  breprexplema  35259  breprexplemc  35261  breprexp  35262  breprexpnat  35263  vtsprod  35268  circlemeth  35269  circlemethnat  35270  circlevma  35271  circlemethhgt  35272  hgt750lemd  35277  hgt750lemb  35285  hgt750lema  35286  subfaclim  35953  fwddifnp1  36930  knoppndvlem6  37383  rrnmet  38763  3factsumint2  43072  3factsumint3  43073  lcmineqlem1  43079  lcmineqlem3  43081  lcmineqlem6  43084  sticksstones8  43203  sticksstones9  43204  sticksstones10  43205  sticksstones11  43206  sticksstones12a  43207  sticksstones12  43208  sticksstones17  43213  sticksstones18  43214  sticksstones19  43215  aks6d1c6lem1  43220  aks6d1c6lem3  43222  aks6d1c7lem3  43232  unitscyglem2  43246  sumcubes  43370  fltnltalem  43673  jm2.22  44001  jm2.23  44002  flcidc  44171  binomcxplemnn0  45332  binomcxplemdvsum  45338  binomcxplemnotnn0  45339  mccllem  46608  isumneg  46613  sumnnodd  46641  dvnmul  46952  dvnprodlem2  46956  dvnprodlem3  46957  stoweidlem37  47046  dirkertrigeqlem2  47108  dirkertrigeqlem3  47109  fourierdlem81  47196  fourierdlem83  47198  fourierdlem93  47208  fourierdlem103  47218  fourierdlem104  47219  elaa2lem  47242  etransclem23  47266  etransclem24  47267  etransclem31  47274  etransclem32  47275  etransclem35  47278  etransclem46  47289  rrxtopnfi  47296  rrndistlt  47299  sge0z  47384  sge0fsummpt  47399  sge0sup  47400  sge0resplit  47415  sge0split  47418  sge0ltfirpmpt2  47435  omeiunltfirp  47528  carageniuncllem2  47531  hoidmvlelem2  47605  hoidmvlelem3  47606  ppivalnn  48716  perfectALTVlem2  48819  nnsum3primesprm  48887  nnsum3primesgbe  48889  nnsum4primeseven  48897  altgsumbc  49463  altgsumbcALT  49464  nn0sumshdiglemA  49730  nn0sumshdiglemB  49731  nn0sumshdig  49734  aacllem  50938  amgmwlem  50986