MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  seqeq1d Structured version   Visualization version   GIF version

Theorem seqeq1d 13367
Description: Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.)
Hypothesis
Ref Expression
seqeqd.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
seqeq1d (𝜑 → seq𝐴( + , 𝐹) = seq𝐵( + , 𝐹))

Proof of Theorem seqeq1d
StepHypRef Expression
1 seqeqd.1 . 2 (𝜑𝐴 = 𝐵)
2 seqeq1 13364 . 2 (𝐴 = 𝐵 → seq𝐴( + , 𝐹) = seq𝐵( + , 𝐹))
31, 2syl 17 1 (𝜑 → seq𝐴( + , 𝐹) = seq𝐵( + , 𝐹))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  seqcseq 13361
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-xp 5554  df-cnv 5556  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-iota 6307  df-fv 6356  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-seq 13362
This theorem is referenced by:  seqeq123d  13370  seqf1olem2  13402  bcval5  13670  bcn2  13671  seqshft  14436  iserex  15005  isershft  15012  isercoll2  15017  isumsplit  15187  cvgrat  15231  ntrivcvg  15245  ntrivcvgtail  15248  fprodser  15295  eftlub  15454  gsumval2a  17887  gsumsgrpccat  17996  gsumccatOLD  17997  mulgnndir  18248  geolim3  24920  fmul01lt1lem2  41855  stirlinglem7  42355  stirlinglem12  42360
  Copyright terms: Public domain W3C validator