Theorem seqeq3d 14179

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-xp 5661  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6322  df-iota 6512  df-fv 6566  df-ov 7446  df-oprab 7447  df-mpo 7448  df-frecs 8327  df-wrecs 8358  df-recs 8407  df-rdg 8446  df-seq 14172

This theorem is used by:  seqeq123d  14180  seqf1olem2  14212  seqf1o  14213  seqof2  14230  expval  14233  relexp1g  15208  sumeq1  15885  sumeq2w  15888  cbvsum  15891  cbvsumv  15892  sumeq2sdv  15899  summo  15912  fsum  15915  geomulcvg  16074  prodeq1f  16104  prodeq1  16105  prodeq2w  16108  prodeq2sdv  16120  prodmo  16132  fprod  16137  gsumvalx  18894  mulgval  19310  gsumval3eu  20148  gsumval3lem2  20150  gsumzres  20153  gsumzf1o  20156  elovolmr  25827  ovolctb  25841  ovoliunlem3  25855  ovoliunnul  25858  ovolshftlem1  25860  voliunlem3  25903  voliun  25905  uniioombllem2  25934  vitalilem4  25962  vitalilem5  25963  dvnfval  26272  mtestbdd  26762  radcnv0  26773  radcnvlt1  26775  radcnvle  26777  psercn  26783  pserdvlem2  26785  abelthlem1  26788  abelthlem3  26790  logtayl  27018  atantayl2  27296  atantayl3  27297  lgamgulm2  27393  lgamcvglem  27397  lgsval  27658  lgsval4  27674  lgsneg  27678  lgsmod  27680  dchrmusumlema  27850  dchrisum0lema  27871  faclim  36689  prodeq12sdv  37185  cbvsumdavw  37246  cbvproddavw  37247  cbvsumdavw2  37262  cbvproddavw2  37263  knoppcnlem9  37545  knoppndvlem4  37559  ovoliunnfl  38772  voliunnfl  38774  radcnvrat  45490  dvradcnv2  45523  binomcxplemcvg  45530  binomcxplemdvsum  45531  binomcxplemnotnn0  45532  sumnnodd  46847  stirlinglem5  47293  sge0isummpt2  47647  ovolval2lem  47858