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

Theorem resss 5302
Description: A class includes its restriction. Exercise 15 of [TakeutiZaring] p. 25. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
resss

Proof of Theorem resss
StepHypRef Expression
1 df-res 5016 . 2
2 inss1 3717 . 2
31, 2eqsstri 3533 1
Colors of variables: wff setvar class
Syntax hints:   cvv 3109  i^icin 3474  C_wss 3475  X.cxp 5002  |`cres 5006
This theorem is referenced by:  relssres  5316  resexg  5321  iss  5326  relresfld  5539  relcoi1  5541  funres  5632  funres11  5661  funcnvres  5662  2elresin  5697  fssres  5756  foimacnv  5838  frxp  6910  fnwelem  6915  tposss  6975  dftpos4  6993  smores  7042  smores2  7044  tfrlem15  7080  finresfin  7765  fidomdm  7822  imafi  7833  marypha1lem  7913  hartogslem1  7988  r0weon  8411  ackbij2lem3  8642  axdc3lem2  8852  smobeth  8982  wunres  9130  vdwnnlem1  14513  symgsssg  16492  symgfisg  16493  psgnunilem5  16519  odf1o2  16593  gsumzres  16914  gsumzresOLD  16918  gsumzaddlem  16934  gsumzadd  16935  gsumzaddlemOLD  16936  gsumzaddOLD  16937  gsum2dlem2  16998  gsum2dOLD  17000  dprdfadd  17060  dprdfaddOLD  17067  dprdres  17075  dprd2dlem1  17090  dprd2da  17091  opsrtoslem2  18149  lindfres  18858  txss12  20106  txbasval  20107  fmss  20447  tsmsresOLD  20645  ustneism  20726  trust  20732  isngp2  21117  equivcau  21739  cmetss  21753  volf  21940  dvcnvrelem1  22418  tdeglem4  22458  pserdv  22824  dvlog  23032  dchrelbas2  23512  uhgrares  24308  umgrares  24324  usgrares  24369  issubgoi  25312  hlimadd  26110  hlimcaui  26154  hhsst  26182  hhsssh2  26186  hhsscms  26195  occllem  26221  nlelchi  26980  hmopidmchi  27070  fnresin  27470  dmct  27537  omsmon  28267  eulerpartlemmf  28314  nodenselem6  29446  funpartss  29594  brresi  30209  bnd2lem  30287  diophrw  30692  dnnumch2  30991  lmhmlnmsplit  31033  hbtlem6  31078  fourierdlem42  31931  fourierdlem80  31969  resisresindm  32305  uhgres  32379
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-ss 3489  df-res 5016
  Copyright terms: Public domain W3C validator