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

Theorem seqeq3d 11362
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 11359 . 2  |-  ( A  =  B  ->  seq  M (  .+  ,  A
)  =  seq  M
(  .+  ,  B
) )
31, 2syl 16 1  |-  ( ph  ->  seq  M (  .+  ,  A )  =  seq  M (  .+  ,  B
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    seq cseq 11354
This theorem is referenced by:  seqeq123d  11363  seqf1olem2  11394  seqf1o  11395  seqof2  11412  expval  11415  sumeq1f  12513  sumeq2w  12517  cbvsum  12520  summo  12542  fsum  12545  geomulcvg  12684  gsumvalx  14805  mulgval  14923  gsumval3eu  15544  gsumval3  15545  gsumzres  15548  gsumzf1o  15550  elovolmr  19403  ovolctb  19417  ovoliunlem3  19431  ovoliunnul  19434  ovolshftlem1  19436  voliunlem3  19477  voliun  19479  uniioombllem2  19506  vitalilem4  19534  vitalilem5  19535  dvnfval  19839  mtestbdd  20352  radcnv0  20363  radcnvlt1  20365  radcnvle  20367  psercn  20373  pserdvlem2  20375  abelthlem1  20378  abelthlem3  20380  logtayl  20582  atantayl2  20809  atantayl3  20810  lgsval  21115  lgsval4  21131  lgsneg  21134  lgsmod  21136  dchrmusumlema  21218  dchrisum0lema  21239  gxval  21877  lgamgulm2  24851  lgamcvglem  24855  prodeq1f  25265  prodeq2w  25269  prodmo  25293  fprod  25298  faclim  25396  ovoliunnfl  26284  voliunnfl  26286  stirlinglem5  27841
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ral 2716  df-rex 2717  df-rab 2720  df-v 2964  df-dif 3309  df-un 3311  df-in 3313  df-ss 3320  df-nul 3614  df-if 3764  df-sn 3844  df-pr 3845  df-op 3847  df-uni 4040  df-br 4238  df-opab 4292  df-mpt 4293  df-cnv 4915  df-dm 4917  df-rn 4918  df-res 4919  df-ima 4920  df-iota 5447  df-fv 5491  df-ov 6113  df-oprab 6114  df-mpt2 6115  df-recs 6662  df-rdg 6697  df-seq 11355
  Copyright terms: Public domain W3C validator