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

Theorem seqeq3d 11806
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 11803 . 2  |-  ( A  =  B  ->  seq M (  .+  ,  A )  =  seq M (  .+  ,  B ) )
31, 2syl 16 1  |-  ( ph  ->  seq M (  .+  ,  A )  =  seq M (  .+  ,  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    seqcseq 11798
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-mpt 4347  df-cnv 4843  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fv 5421  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-recs 6824  df-rdg 6858  df-seq 11799
This theorem is referenced by:  seqeq123d  11807  seqf1olem2  11838  seqf1o  11839  seqof2  11856  expval  11859  sumeq1  13158  sumeq2w  13161  cbvsum  13164  summo  13186  fsum  13189  geomulcvg  13328  gsumvalx  15493  mulgval  15620  gsumval3eu  16372  gsumval3OLD  16373  gsumval3lem2  16375  gsumzres  16379  gsumzf1o  16382  gsumzresOLD  16383  gsumzf1oOLD  16385  elovolmr  20934  ovolctb  20948  ovoliunlem3  20962  ovoliunnul  20965  ovolshftlem1  20967  voliunlem3  21008  voliun  21010  uniioombllem2  21038  vitalilem4  21066  vitalilem5  21067  dvnfval  21371  mtestbdd  21845  radcnv0  21856  radcnvlt1  21858  radcnvle  21860  psercn  21866  pserdvlem2  21868  abelthlem1  21871  abelthlem3  21873  logtayl  22080  atantayl2  22308  atantayl3  22309  lgsval  22614  lgsval4  22630  lgsneg  22633  lgsmod  22635  dchrmusumlema  22717  dchrisum0lema  22738  gxval  23696  lgamgulm2  26974  lgamcvglem  26978  prodeq1f  27372  prodeq2w  27376  prodmo  27400  fprod  27405  faclim  27503  ovoliunnfl  28386  voliunnfl  28388  stirlinglem5  29826
  Copyright terms: Public domain W3C validator