Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  seqeq2 Structured version   Unicode version

Theorem seqeq2 11913
 Description: Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.)
Assertion
Ref Expression
seqeq2

Proof of Theorem seqeq2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqidd 2452 . . . . 5
2 oveq 6198 . . . . . 6
32opeq2d 4166 . . . . 5
41, 1, 3mpt2eq123dv 6249 . . . 4
5 rdgeq1 6969 . . . 4
64, 5syl 16 . . 3
76imaeq1d 5268 . 2
8 df-seq 11910 . 2
9 df-seq 11910 . 2
107, 8, 93eqtr4g 2517 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wceq 1370  cvv 3070  cop 3983  cima 4943  cfv 5518  (class class class)co 6192   cmpt2 6194  com 6578  crdg 6967  c1 9386   caddc 9388   cseq 11909 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3072  df-dif 3431  df-un 3433  df-in 3435  df-ss 3442  df-nul 3738  df-if 3892  df-sn 3978  df-pr 3980  df-op 3984  df-uni 4192  df-br 4393  df-opab 4451  df-mpt 4452  df-cnv 4948  df-dm 4950  df-rn 4951  df-res 4952  df-ima 4953  df-iota 5481  df-fv 5526  df-ov 6195  df-oprab 6196  df-mpt2 6197  df-recs 6934  df-rdg 6968  df-seq 11910 This theorem is referenced by:  seqeq2d  11916  sadcom  13763  gxfval  23881  ressmulgnn  26280  cvmliftlem15  27323
 Copyright terms: Public domain W3C validator