Theorem seqeq3d 12809

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

Syntax hints:   → wi 4   = wceq 1483  seqcseq 12801

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-xp 5120  df-cnv 5122  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-iota 5851  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-seq 12802

This theorem is referenced by:  seqeq123d  12810  seqf1olem2  12841  seqf1o  12842  seqof2  12859  expval  12862  relexp1g  13766  sumeq1  14419  sumeq2w  14422  cbvsum  14425  summo  14448  fsum  14451  geomulcvg  14607  prodeq1f  14638  prodeq2w  14642  prodmo  14666  fprod  14671  gsumvalx  17270  mulgval  17543  gsumval3eu  18305  gsumval3lem2  18307  gsumzres  18310  gsumzf1o  18313  elovolmr  23244  ovolctb  23258  ovoliunlem3  23272  ovoliunnul  23275  ovolshftlem1  23277  voliunlem3  23320  voliun  23322  uniioombllem2  23351  vitalilem4  23380  vitalilem5  23381  dvnfval  23685  mtestbdd  24159  radcnv0  24170  radcnvlt1  24172  radcnvle  24174  psercn  24180  pserdvlem2  24182  abelthlem1  24185  abelthlem3  24187  logtayl  24406  atantayl2  24665  atantayl3  24666  lgamgulm2  24762  lgamcvglem  24766  lgsval  25026  lgsval4  25042  lgsneg  25046  lgsmod  25048  dchrmusumlema  25182  dchrisum0lema  25203  faclim  31632  knoppcnlem9  32491  knoppndvlem4  32506  ovoliunnfl  33451  voliunnfl  33453  radcnvrat  38513  dvradcnv2  38546  binomcxplemcvg  38553  binomcxplemdvsum  38554  binomcxplemnotnn0  38555  sumnnodd  39862  stirlinglem5  40295  sge0isummpt2  40649  ovolval2lem  40857