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

Theorem seqeq3d 12118
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 12115 . 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 1395    seqcseq 12110
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-br 4457  df-opab 4516  df-mpt 4517  df-cnv 5016  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fv 5602  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-recs 7060  df-rdg 7094  df-seq 12111
This theorem is referenced by:  seqeq123d  12119  seqf1olem2  12150  seqf1o  12151  seqof2  12168  expval  12171  sumeq1  13523  sumeq2w  13526  cbvsum  13529  summo  13551  fsum  13554  geomulcvg  13697  prodeq1f  13727  prodeq2w  13731  prodmo  13755  fprod  13760  gsumvalx  16024  mulgval  16271  gsumval3eu  17034  gsumval3OLD  17035  gsumval3lem2  17037  gsumzres  17041  gsumzf1o  17044  gsumzresOLD  17045  gsumzf1oOLD  17047  elovolmr  22013  ovolctb  22027  ovoliunlem3  22041  ovoliunnul  22044  ovolshftlem1  22046  voliunlem3  22088  voliun  22090  uniioombllem2  22118  vitalilem4  22146  vitalilem5  22147  dvnfval  22451  mtestbdd  22926  radcnv0  22937  radcnvlt1  22939  radcnvle  22941  psercn  22947  pserdvlem2  22949  abelthlem1  22952  abelthlem3  22954  logtayl  23167  atantayl2  23395  atantayl3  23396  lgsval  23701  lgsval4  23717  lgsneg  23720  lgsmod  23722  dchrmusumlema  23804  dchrisum0lema  23825  gxval  25387  lgamgulm2  28775  lgamcvglem  28779  relexp1g  29253  faclim  29389  ovoliunnfl  30261  voliunnfl  30263  radcnvrat  31399  dvradcnv2  31456  binomcxplemcvg  31463  binomcxplemdvsum  31464  binomcxplemnotnn0  31465  sumnnodd  31839  stirlinglem5  32063
  Copyright terms: Public domain W3C validator