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

Step	Hyp	Ref	Expression
1		seqeqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		seqeq1 13463	. 2 ⊢ (𝐴 = 𝐵 → seq𝐴( + , 𝐹) = seq𝐵( + , 𝐹))
3	1, 2	syl 17	1 ⊢ (𝜑 → seq𝐴( + , 𝐹) = seq𝐵( + , 𝐹))

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