Theorem seqeq3d 13738

Description: Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.)

Hypothesis

Ref	Expression
seqeqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
seqeq3d	⊢ (𝜑 → seq𝑀( + , 𝐴) = seq𝑀( + , 𝐵))

Proof of Theorem seqeq3d

Step	Hyp	Ref	Expression
1		seqeqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		seqeq3 13735	. 2 ⊢ (𝐴 = 𝐵 → seq𝑀( + , 𝐴) = seq𝑀( + , 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → seq𝑀( + , 𝐴) = seq𝑀( + , 𝐵))

Syntax hints:   → wi 4   = wceq 1539  seqcseq 13730

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-mpt 5159  df-xp 5596  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-iota 6395  df-fv 6445  df-ov 7287  df-oprab 7288  df-mpo 7289  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-seq 13731

This theorem is referenced by:  seqeq123d  13739  seqf1olem2  13772  seqf1o  13773  seqof2  13790  expval  13793  relexp1g  14746  sumeq1  15409  sumeq2w  15413  cbvsum  15416  summo  15438  fsum  15441  geomulcvg  15597  prodeq1f  15627  prodeq2w  15631  prodmo  15655  fprod  15660  gsumvalx  18369  mulgval  18713  gsumval3eu  19514  gsumval3lem2  19516  gsumzres  19519  gsumzf1o  19522  elovolmr  24649  ovolctb  24663  ovoliunlem3  24677  ovoliunnul  24680  ovolshftlem1  24682  voliunlem3  24725  voliun  24727  uniioombllem2  24756  vitalilem4  24784  vitalilem5  24785  dvnfval  25095  mtestbdd  25573  radcnv0  25584  radcnvlt1  25586  radcnvle  25588  psercn  25594  pserdvlem2  25596  abelthlem1  25599  abelthlem3  25601  logtayl  25824  atantayl2  26097  atantayl3  26098  lgamgulm2  26194  lgamcvglem  26198  lgsval  26458  lgsval4  26474  lgsneg  26478  lgsmod  26480  dchrmusumlema  26650  dchrisum0lema  26671  faclim  33721  knoppcnlem9  34690  knoppndvlem4  34704  ovoliunnfl  35828  voliunnfl  35830  radcnvrat  41939  dvradcnv2  41972  binomcxplemcvg  41979  binomcxplemdvsum  41980  binomcxplemnotnn0  41981  sumnnodd  43178  stirlinglem5  43626  sge0isummpt2  43977  ovolval2lem  44188