Theorem seqeq3d 13657

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

Syntax hints:   → wi 4   = wceq 1539  seqcseq 13649

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-xp 5586  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-iota 6376  df-fv 6426  df-ov 7258  df-oprab 7259  df-mpo 7260  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-seq 13650

This theorem is referenced by:  seqeq123d  13658  seqf1olem2  13691  seqf1o  13692  seqof2  13709  expval  13712  relexp1g  14665  sumeq1  15328  sumeq2w  15332  cbvsum  15335  summo  15357  fsum  15360  geomulcvg  15516  prodeq1f  15546  prodeq2w  15550  prodmo  15574  fprod  15579  gsumvalx  18275  mulgval  18619  gsumval3eu  19420  gsumval3lem2  19422  gsumzres  19425  gsumzf1o  19428  elovolmr  24545  ovolctb  24559  ovoliunlem3  24573  ovoliunnul  24576  ovolshftlem1  24578  voliunlem3  24621  voliun  24623  uniioombllem2  24652  vitalilem4  24680  vitalilem5  24681  dvnfval  24991  mtestbdd  25469  radcnv0  25480  radcnvlt1  25482  radcnvle  25484  psercn  25490  pserdvlem2  25492  abelthlem1  25495  abelthlem3  25497  logtayl  25720  atantayl2  25993  atantayl3  25994  lgamgulm2  26090  lgamcvglem  26094  lgsval  26354  lgsval4  26370  lgsneg  26374  lgsmod  26376  dchrmusumlema  26546  dchrisum0lema  26567  faclim  33618  knoppcnlem9  34608  knoppndvlem4  34622  ovoliunnfl  35746  voliunnfl  35748  radcnvrat  41821  dvradcnv2  41854  binomcxplemcvg  41861  binomcxplemdvsum  41862  binomcxplemnotnn0  41863  sumnnodd  43061  stirlinglem5  43509  sge0isummpt2  43860  ovolval2lem  44071