MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  seqeq3d Structured version   Visualization version   GIF version

Theorem seqeq3d 13371
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
StepHypRef Expression
1 seqeqd.1 . 2 (𝜑𝐴 = 𝐵)
2 seqeq3 13368 . 2 (𝐴 = 𝐵 → seq𝑀( + , 𝐴) = seq𝑀( + , 𝐵))
31, 2syl 17 1 (𝜑 → seq𝑀( + , 𝐴) = seq𝑀( + , 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1533  seqcseq 13363
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-br 5059  df-opab 5121  df-mpt 5139  df-xp 5555  df-cnv 5557  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-iota 6308  df-fv 6357  df-ov 7153  df-oprab 7154  df-mpo 7155  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-seq 13364
This theorem is referenced by:  seqeq123d  13372  seqf1olem2  13404  seqf1o  13405  seqof2  13422  expval  13425  relexp1g  14379  sumeq1  15039  sumeq2w  15043  cbvsum  15046  summo  15068  fsum  15071  geomulcvg  15226  prodeq1f  15256  prodeq2w  15260  prodmo  15284  fprod  15289  gsumvalx  17880  mulgval  18222  gsumval3eu  19018  gsumval3lem2  19020  gsumzres  19023  gsumzf1o  19026  elovolmr  24071  ovolctb  24085  ovoliunlem3  24099  ovoliunnul  24102  ovolshftlem1  24104  voliunlem3  24147  voliun  24149  uniioombllem2  24178  vitalilem4  24206  vitalilem5  24207  dvnfval  24513  mtestbdd  24987  radcnv0  24998  radcnvlt1  25000  radcnvle  25002  psercn  25008  pserdvlem2  25010  abelthlem1  25013  abelthlem3  25015  logtayl  25237  atantayl2  25510  atantayl3  25511  lgamgulm2  25607  lgamcvglem  25611  lgsval  25871  lgsval4  25887  lgsneg  25891  lgsmod  25893  dchrmusumlema  26063  dchrisum0lema  26084  faclim  32973  knoppcnlem9  33835  knoppndvlem4  33849  ovoliunnfl  34928  voliunnfl  34930  radcnvrat  40639  dvradcnv2  40672  binomcxplemcvg  40679  binomcxplemdvsum  40680  binomcxplemnotnn0  40681  sumnnodd  41904  stirlinglem5  42357  sge0isummpt2  42708  ovolval2lem  42919
  Copyright terms: Public domain W3C validator