Theorem seqeq3d 14155

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  seqcseq 14147

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-xp 5656  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-iota 6494  df-fv 6546  df-ov 7423  df-oprab 7424  df-mpo 7425  df-frecs 8302  df-wrecs 8333  df-recs 8382  df-rdg 8421  df-seq 14148

This theorem is used by:  seqeq123d  14156  seqf1olem2  14188  seqf1o  14189  seqof2  14206  expval  14209  relexp1g  15184  sumeq1  15861  sumeq2w  15864  cbvsum  15867  cbvsumv  15868  sumeq2sdv  15875  summo  15888  fsum  15891  geomulcvg  16050  prodeq1f  16080  prodeq1  16081  prodeq2w  16084  prodeq2sdv  16096  prodmo  16108  fprod  16113  gsumvalx  18870  mulgval  19286  gsumval3eu  20123  gsumval3lem2  20125  gsumzres  20128  gsumzf1o  20131  elovolmr  25802  ovolctb  25816  ovoliunlem3  25830  ovoliunnul  25833  ovolshftlem1  25835  voliunlem3  25878  voliun  25880  uniioombllem2  25909  vitalilem4  25937  vitalilem5  25938  dvnfval  26247  mtestbdd  26737  radcnv0  26748  radcnvlt1  26750  radcnvle  26752  psercn  26758  pserdvlem2  26760  abelthlem1  26763  abelthlem3  26765  logtayl  26993  atantayl2  27271  atantayl3  27272  lgamgulm2  27368  lgamcvglem  27372  lgsval  27633  lgsval4  27649  lgsneg  27653  lgsmod  27655  dchrmusumlema  27825  dchrisum0lema  27846  faclim  36603  prodeq12sdv  37099  cbvsumdavw  37160  cbvproddavw  37161  cbvsumdavw2  37176  cbvproddavw2  37177  knoppcnlem9  37459  knoppndvlem4  37473  ovoliunnfl  38673  voliunnfl  38675  radcnvrat  45391  dvradcnv2  45424  binomcxplemcvg  45431  binomcxplemdvsum  45432  binomcxplemnotnn0  45433  sumnnodd  46735  stirlinglem5  47181  sge0isummpt2  47535  ovolval2lem  47746