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

Theorem reseq1 5272
Description: Equality theorem for restrictions. (Contributed by NM, 7-Aug-1994.)
Assertion
Ref Expression
reseq1

Proof of Theorem reseq1
StepHypRef Expression
1 ineq1 3692 . 2
2 df-res 5016 . 2
3 df-res 5016 . 2
41, 2, 33eqtr4g 2523 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395   cvv 3109  i^icin 3474  X.cxp 5002  |`cres 5006
This theorem is referenced by:  reseq1i  5274  reseq1d  5277  imaeq1  5337  relcoi1  5541  fvtresfn  5957  tfrlem12  7077  pmresg  7466  resixpfo  7527  mapunen  7706  fseqenlem1  8426  axdc3lem2  8852  axdc3lem4  8854  axdc  8922  hashf1lem1  12504  lo1eq  13391  rlimeq  13392  symgfixfo  16464  lspextmo  17702  evlseu  18185  mdetunilem3  19116  mdetunilem4  19117  mdetunilem9  19122  lmbr  19759  ptuncnv  20308  iscau  21715  plyexmo  22709  relogf1o  22954  isdivrngo  25433  eulerpartlemt  28310  eulerpartlemgv  28312  eulerpartlemn  28320  eulerpart  28321  iscvm  28704  ghomgrplem  29029  trpredlem1  29310  trpredtr  29313  trpredmintr  29314  wfrlem1  29343  wfrlem15  29357  frrlem1  29387  nofulllem5  29466  mbfresfi  30061  eqfnun  30212  sdclem2  30235  mzpcompact2lem  30684  diophrw  30692  eldioph2lem1  30693  eldioph2lem2  30694  eldioph3  30699  diophin  30706  diophrex  30709  rexrabdioph  30727  2rexfrabdioph  30729  3rexfrabdioph  30730  4rexfrabdioph  30731  6rexfrabdioph  30732  7rexfrabdioph  30733  eldioph4b  30745  pwssplit4  31035  dvnprodlem1  31743  dvnprodlem3  31745  bnj1385  33891  bnj66  33918  bnj1234  34069  bnj1326  34082  bnj1463  34111
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3482  df-res 5016
  Copyright terms: Public domain W3C validator