Theorem seqeq3d 14077

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

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

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 2734

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 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-xp 5665  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-iota 6493  df-fv 6545  df-ov 7420  df-oprab 7421  df-mpo 7422  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-seq 14070

This theorem is used by:  seqeq123d  14078  seqf1olem2  14110  seqf1o  14111  seqof2  14128  expval  14131  relexp1g  15103  sumeq1  15780  sumeq2w  15783  cbvsum  15786  cbvsumv  15787  sumeq2sdv  15794  summo  15807  fsum  15810  geomulcvg  15969  prodeq1f  15999  prodeq1  16000  prodeq2w  16003  prodeq2sdv  16016  prodmo  16029  fprod  16034  gsumvalx  18784  mulgval  19200  gsumval3eu  20037  gsumval3lem2  20039  gsumzres  20042  gsumzf1o  20045  elovolmr  25710  ovolctb  25724  ovoliunlem3  25738  ovoliunnul  25741  ovolshftlem1  25743  voliunlem3  25786  voliun  25788  uniioombllem2  25817  vitalilem4  25845  vitalilem5  25846  dvnfval  26156  mtestbdd  26648  radcnv0  26659  radcnvlt1  26661  radcnvle  26663  psercn  26669  pserdvlem2  26671  abelthlem1  26674  abelthlem3  26676  logtayl  26905  atantayl2  27183  atantayl3  27184  lgamgulm2  27280  lgamcvglem  27284  lgsval  27545  lgsval4  27561  lgsneg  27565  lgsmod  27567  dchrmusumlema  27737  dchrisum0lema  27758  faclim  36333  prodeq12sdv  36846  cbvsumdavw  36907  cbvproddavw  36908  cbvsumdavw2  36923  cbvproddavw2  36924  knoppcnlem9  37206  knoppndvlem4  37220  ovoliunnfl  38419  voliunnfl  38421  radcnvrat  45146  dvradcnv2  45179  binomcxplemcvg  45186  binomcxplemdvsum  45187  binomcxplemnotnn0  45188  sumnnodd  46468  stirlinglem5  46914  sge0isummpt2  47268  ovolval2lem  47479