Theorem seqeq3d 14132

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 14129	. 2 ⊢ (𝐴 = 𝐵 → seq𝑀( + , 𝐴) = seq𝑀( + , 𝐵))
3	1, 2	syl 18	1 ⊢ (𝜑 → seq𝑀( + , 𝐴) = seq𝑀( + , 𝐵))

This proof depends on syntax axioms:   → wi 4   = wceq 1570  seqcseq 14124

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-xp 5657  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6297  df-iota 6487  df-fv 6539  df-ov 7415  df-oprab 7416  df-mpo 7417  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-seq 14125

This theorem is used by:  seqeq123d  14133  seqf1olem2  14165  seqf1o  14166  seqof2  14183  expval  14186  relexp1g  15159  sumeq1  15836  sumeq2w  15839  cbvsum  15842  cbvsumv  15843  sumeq2sdv  15850  summo  15863  fsum  15866  geomulcvg  16025  prodeq1f  16055  prodeq1  16056  prodeq2w  16059  prodeq2sdv  16071  prodmo  16083  fprod  16088  gsumvalx  18845  mulgval  19261  gsumval3eu  20098  gsumval3lem2  20100  gsumzres  20103  gsumzf1o  20106  elovolmr  25777  ovolctb  25791  ovoliunlem3  25805  ovoliunnul  25808  ovolshftlem1  25810  voliunlem3  25853  voliun  25855  uniioombllem2  25884  vitalilem4  25912  vitalilem5  25913  dvnfval  26222  mtestbdd  26714  radcnv0  26725  radcnvlt1  26727  radcnvle  26729  psercn  26735  pserdvlem2  26737  abelthlem1  26740  abelthlem3  26742  logtayl  26970  atantayl2  27248  atantayl3  27249  lgamgulm2  27345  lgamcvglem  27349  lgsval  27610  lgsval4  27626  lgsneg  27630  lgsmod  27632  dchrmusumlema  27802  dchrisum0lema  27823  faclim  36480  prodeq12sdv  36977  cbvsumdavw  37038  cbvproddavw  37039  cbvsumdavw2  37054  cbvproddavw2  37055  knoppcnlem9  37337  knoppndvlem4  37351  ovoliunnfl  38548  voliunnfl  38550  radcnvrat  45257  dvradcnv2  45290  binomcxplemcvg  45297  binomcxplemdvsum  45298  binomcxplemnotnn0  45299  sumnnodd  46586  stirlinglem5  47032  sge0isummpt2  47386  ovolval2lem  47597