Theorem seqeq3d 13978

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

Syntax hints:   → wi 4   = wceq 1539  seqcseq 13970

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-xp 5681  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-iota 6494  df-fv 6550  df-ov 7414  df-oprab 7415  df-mpo 7416  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-seq 13971

This theorem is referenced by:  seqeq123d  13979  seqf1olem2  14012  seqf1o  14013  seqof2  14030  expval  14033  relexp1g  14977  sumeq1  15639  sumeq2w  15642  cbvsum  15645  summo  15667  fsum  15670  geomulcvg  15826  prodeq1f  15856  prodeq2w  15860  prodmo  15884  fprod  15889  gsumvalx  18601  mulgval  18990  gsumval3eu  19813  gsumval3lem2  19815  gsumzres  19818  gsumzf1o  19821  elovolmr  25225  ovolctb  25239  ovoliunlem3  25253  ovoliunnul  25256  ovolshftlem1  25258  voliunlem3  25301  voliun  25303  uniioombllem2  25332  vitalilem4  25360  vitalilem5  25361  dvnfval  25672  mtestbdd  26153  radcnv0  26164  radcnvlt1  26166  radcnvle  26168  psercn  26174  pserdvlem2  26176  abelthlem1  26179  abelthlem3  26181  logtayl  26404  atantayl2  26679  atantayl3  26680  lgamgulm2  26776  lgamcvglem  26780  lgsval  27040  lgsval4  27056  lgsneg  27060  lgsmod  27062  dchrmusumlema  27232  dchrisum0lema  27253  faclim  35020  knoppcnlem9  35680  knoppndvlem4  35694  ovoliunnfl  36833  voliunnfl  36835  radcnvrat  43375  dvradcnv2  43408  binomcxplemcvg  43415  binomcxplemdvsum  43416  binomcxplemnotnn0  43417  sumnnodd  44644  stirlinglem5  45092  sge0isummpt2  45446  ovolval2lem  45657