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

Theorem seqeq1d 13466
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 13463 . 2 (𝐴 = 𝐵 → seq𝐴( + , 𝐹) = seq𝐵( + , 𝐹))
31, 2syl 17 1 (𝜑 → seq𝐴( + , 𝐹) = seq𝐵( + , 𝐹))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  seqcseq 13460
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-12 2179  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-ex 1787  df-nf 1791  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-ral 3058  df-rab 3062  df-v 3400  df-un 3848  df-in 3850  df-ss 3860  df-if 4415  df-sn 4517  df-pr 4519  df-op 4523  df-uni 4797  df-br 5031  df-opab 5093  df-mpt 5111  df-xp 5531  df-cnv 5533  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6129  df-iota 6297  df-fv 6347  df-wrecs 7976  df-recs 8037  df-rdg 8075  df-seq 13461
This theorem is referenced by:  seqeq123d  13469  seqf1olem2  13502  bcval5  13770  bcn2  13771  seqshft  14534  iserex  15106  isershft  15113  isercoll2  15118  isumsplit  15288  cvgrat  15331  ntrivcvg  15345  ntrivcvgtail  15348  fprodser  15395  eftlub  15554  gsumval2a  18011  gsumsgrpccat  18120  gsumccatOLD  18121  mulgnndir  18374  geolim3  25087  fmul01lt1lem2  42668  stirlinglem7  43163  stirlinglem12  43168
  Copyright terms: Public domain W3C validator