MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  seqeq3d Unicode version

Theorem seqeq3d 11218
Description: Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.)
Hypothesis
Ref Expression
seqeqd.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
seqeq3d  |-  ( ph  ->  seq  M (  .+  ,  A )  =  seq  M (  .+  ,  B
) )

Proof of Theorem seqeq3d
StepHypRef Expression
1 seqeqd.1 . 2  |-  ( ph  ->  A  =  B )
2 seqeq3 11215 . 2  |-  ( A  =  B  ->  seq  M (  .+  ,  A
)  =  seq  M
(  .+  ,  B
) )
31, 2syl 15 1  |-  ( ph  ->  seq  M (  .+  ,  A )  =  seq  M (  .+  ,  B
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1647    seq cseq 11210
This theorem is referenced by:  seqeq123d  11219  seqf1olem2  11250  seqf1o  11251  seqof2  11268  expval  11271  sumeq1f  12369  sumeq2w  12373  cbvsum  12376  summo  12398  fsum  12401  geomulcvg  12540  gsumvalx  14661  mulgval  14779  gsumval3eu  15400  gsumval3  15401  gsumzres  15404  gsumzf1o  15406  elovolmr  19050  ovolctb  19064  ovoliunlem3  19078  ovoliunnul  19081  ovolshftlem1  19083  voliunlem3  19124  voliun  19126  uniioombllem2  19153  vitalilem4  19181  vitalilem5  19182  dvnfval  19486  mtestbdd  19999  radcnv0  20010  radcnvlt1  20012  radcnvle  20014  psercn  20020  pserdvlem2  20022  abelthlem1  20025  abelthlem3  20027  logtayl  20229  atantayl2  20456  atantayl3  20457  lgsval  20762  lgsval4  20778  lgsneg  20781  lgsmod  20783  dchrmusumlema  20865  dchrisum0lema  20886  gxval  21236  lgamgulm2  24268  lgamcvglem  24272  prodeq1f  24718  prodeq2w  24722  prodmo  24746  fprod  24751  faclim  24840  ovoliunnfl  25671  voliunnfl  25673  stirlinglem5  27333
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ral 2633  df-rex 2634  df-rab 2637  df-v 2875  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-nul 3544  df-if 3655  df-sn 3735  df-pr 3736  df-op 3738  df-uni 3930  df-br 4126  df-opab 4180  df-mpt 4181  df-cnv 4800  df-dm 4802  df-rn 4803  df-res 4804  df-ima 4805  df-iota 5322  df-fv 5366  df-ov 5984  df-oprab 5985  df-mpt2 5986  df-recs 6530  df-rdg 6565  df-seq 11211
  Copyright terms: Public domain W3C validator