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

Theorem seqeq3d 12079
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 12076 . 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 1379    seqcseq 12071
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-mpt 4507  df-cnv 5007  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fv 5594  df-ov 6285  df-oprab 6286  df-mpt2 6287  df-recs 7039  df-rdg 7073  df-seq 12072
This theorem is referenced by:  seqeq123d  12080  seqf1olem2  12111  seqf1o  12112  seqof2  12129  expval  12132  sumeq1  13470  sumeq2w  13473  cbvsum  13476  summo  13498  fsum  13501  geomulcvg  13644  gsumvalx  15815  mulgval  15944  gsumval3eu  16698  gsumval3OLD  16699  gsumval3lem2  16701  gsumzres  16705  gsumzf1o  16708  gsumzresOLD  16709  gsumzf1oOLD  16711  elovolmr  21622  ovolctb  21636  ovoliunlem3  21650  ovoliunnul  21653  ovolshftlem1  21655  voliunlem3  21697  voliun  21699  uniioombllem2  21727  vitalilem4  21755  vitalilem5  21756  dvnfval  22060  mtestbdd  22534  radcnv0  22545  radcnvlt1  22547  radcnvle  22549  psercn  22555  pserdvlem2  22557  abelthlem1  22560  abelthlem3  22562  logtayl  22769  atantayl2  22997  atantayl3  22998  lgsval  23303  lgsval4  23319  lgsneg  23322  lgsmod  23324  dchrmusumlema  23406  dchrisum0lema  23427  gxval  24936  lgamgulm2  28218  lgamcvglem  28222  prodeq1f  28617  prodeq2w  28621  prodmo  28645  fprod  28650  faclim  28748  ovoliunnfl  29633  voliunnfl  29635  sumnnodd  31172  stirlinglem5  31378
  Copyright terms: Public domain W3C validator