Theorem sumeq2dv 15749

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 15748	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  Σcsu 15733

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-cnex 11151  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171  ax-pre-mulgt0 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  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 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7859  df-1st 7982  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244  df-sub 11438  df-neg 11439  df-nn 12229  df-n0 12500  df-z 12587  df-uz 12858  df-fz 13531  df-seq 14034  df-sum 15734

This theorem is referenced by:  2sumeq2dv  15752  sumeq12dv  15753  sumeq12rdv  15754  fsumf1o  15770  fsumss  15772  fsumsplit  15788  isummulc1  15810  isumdivc  15811  isumge0  15813  fsum2dlem  15817  fsumshftm  15828  fsum0diag2  15830  fsummulc1  15832  fsumdivc  15833  fsumneg  15834  fsumsub  15835  fsum2mul  15836  telfsumo2  15851  fsumparts  15854  hashiun  15870  hash2iun  15871  hash2iun1dif1  15872  indsum  15876  ackbijnn  15878  binomlem  15879  binom1p  15881  incexclem  15886  incexc  15887  incexc2  15888  isum1p  15891  arisum  15910  trireciplem  15912  geoserg  15916  pwdif  15918  geo2sum  15923  mertenslem1  15934  mertenslem2  15935  mertens  15936  binomfallfaclem2  16089  binomrisefac  16091  bpolylem  16097  bpolydiflem  16103  fsumkthpow  16105  efaddlem  16142  rpnnen2lem10  16274  rpnnen2lem11  16275  fsumdvds  16361  pwp1fsum  16444  phisum  16845  pcfac  16954  ramcl  17084  lagsubg2  19260  sylow2a  19684  rrxcph  25551  trirn  25559  rrxmval  25564  rrxmet  25567  ovoliunnul  25666  ovolicc2lem4  25679  uniioombllem4  25745  vitalilem5  25771  itg1addlem4  25858  itg1addlem5  25859  itg1mulc  25863  itg10a  25869  itg1climres  25873  itgss  25971  itgeqa  25973  itgsplit  25995  elply2  26353  elplyd  26359  plyeq0lem  26367  plyaddlem1  26370  plymullem1  26371  coeeulem  26381  coeeq2  26399  coemullem  26407  coe1termlem  26415  plycjlem  26433  plyrecj  26438  plyn0mulidp  26442  dvply1  26445  elqaalem3  26482  aareccl  26489  aannenlem1  26491  taylpval  26530  dvtaylp  26533  pserdvlem2  26591  pserdv2  26593  abelthlem8  26602  abelthlem9  26603  abelth  26604  logtayl  26825  leibpi  27107  birthdaylem2  27117  amgmlem  27154  emcllem5  27164  fsumharmonic  27176  lgamcvg2  27219  ftalem5  27241  basellem3  27247  basellem8  27252  sgmval2  27307  fsumdvdscom  27349  dvdsflsumcom  27352  musum  27355  musumsum  27356  muinv  27357  fsumdvdsmul  27359  sgmppw  27361  1sgmprm  27363  chtlepsi  27370  pclogsum  27379  vmasum  27380  logfac2  27381  chpval2  27382  chpchtsum  27383  logexprlim  27389  logfacrlim2  27390  perfectlem2  27394  dchrsum2  27432  sumdchr2  27434  dchrhash  27435  dchr2sum  27437  sum2dchr  27438  pcbcctr  27440  bposlem2  27449  lgsquadlem1  27544  lgsquadlem2  27545  chebbnd1lem1  27633  rplogsumlem1  27648  rplogsumlem2  27649  rpvmasumlem  27651  dchrisumlem1  27653  dchrisumlem2  27654  dchrmusum2  27658  dchrvmasumlem1  27659  dchrvmasum2lem  27660  dchrvmasum2if  27661  dchrvmasumiflem1  27665  dchrvmasumiflem2  27666  dchrisum0flblem1  27672  dchrisum0fno1  27675  rpvmasum2  27676  dchrisum0lem2a  27681  dchrisum0lem2  27682  dchrisum0lem3  27683  dchrisum0  27684  rplogsum  27691  mudivsum  27694  mulogsumlem  27695  mulogsum  27696  mulog2sumlem1  27698  mulog2sumlem2  27699  mulog2sumlem3  27700  vmalogdivsum2  27702  vmalogdivsum  27703  2vmadivsumlem  27704  logsqvma  27706  logsqvma2  27707  selberglem1  27709  selberglem2  27710  selberg  27712  selberg2  27715  selberg3lem1  27721  selberg4lem1  27724  selberg4  27725  pntrsumo1  27729  selbergr  27732  selberg3r  27733  selberg4r  27734  selberg34r  27735  pntsval2  27740  pntrlog2bndlem4  27744  pntrlog2bndlem5  27745  pntpbnd1  27750  pntlemk  27770  pntlemo  27771  axcgrrflx  29264  axcgrid  29266  axsegconlem1  29267  axsegconlem9  29275  ax5seglem1  29278  ax5seglem2  29279  ax5seglem9  29287  axlowdimlem16  29307  axlowdimlem17  29308  ecgrtg  29333  finsumvtxdg2ssteplem3  29897  rusgrnumwwlks  30326  fusgrhashclwwlkn  30430  fusgreghash2wsp  30689  numclwwlk6  30741  indsumin  33181  elrgspnlem2  33563  vietadeg1  33968  eulerpartlemsv1  34746  eulerpartlemsf  34749  eulerpartlemgs2  34770  eulerpartlemn  34771  signsvfn  34969  fsum2dsub  34994  reprsuc  35002  hashreprin  35007  reprpmtf1o  35013  breprexplema  35017  breprexplemc  35019  breprexp  35020  breprexpnat  35021  vtsprod  35026  circlemeth  35027  circlemethnat  35028  circlevma  35029  circlemethhgt  35030  hgt750lemd  35035  hgt750lemb  35043  hgt750lema  35044  subfaclim  35680  fwddifnp1  36657  knoppndvlem6  37126  rrnmet  38500  3factsumint2  42809  3factsumint3  42810  lcmineqlem1  42816  lcmineqlem3  42818  lcmineqlem6  42821  sticksstones8  42940  sticksstones9  42941  sticksstones10  42942  sticksstones11  42943  sticksstones12a  42944  sticksstones12  42945  sticksstones17  42950  sticksstones18  42951  sticksstones19  42952  aks6d1c6lem1  42957  aks6d1c6lem3  42959  aks6d1c7lem3  42969  unitscyglem2  42983  sumcubes  43094  fltnltalem  43414  jm2.22  43742  jm2.23  43743  flcidc  43917  binomcxplemnn0  45079  binomcxplemdvsum  45085  binomcxplemnotnn0  45086  mccllem  46333  isumneg  46338  sumnnodd  46366  dvnmul  46677  dvnprodlem2  46681  dvnprodlem3  46682  stoweidlem37  46771  dirkertrigeqlem2  46833  dirkertrigeqlem3  46834  fourierdlem81  46921  fourierdlem83  46923  fourierdlem93  46933  fourierdlem103  46943  fourierdlem104  46944  elaa2lem  46967  etransclem23  46991  etransclem24  46992  etransclem31  46999  etransclem32  47000  etransclem35  47003  etransclem46  47014  rrxtopnfi  47021  rrndistlt  47024  sge0z  47109  sge0fsummpt  47124  sge0sup  47125  sge0resplit  47140  sge0split  47143  sge0ltfirpmpt2  47160  omeiunltfirp  47253  carageniuncllem2  47256  hoidmvlelem2  47330  hoidmvlelem3  47331  ppivalnn  48404  perfectALTVlem2  48507  nnsum3primesprm  48575  nnsum3primesgbe  48577  nnsum4primeseven  48585  altgsumbc  49152  altgsumbcALT  49153  nn0sumshdiglemA  49419  nn0sumshdiglemB  49420  nn0sumshdig  49423  aacllem  50641  amgmwlem  50669