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

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

Proof of Theorem resss
StepHypRef Expression
1 df-res 4701 . 2  |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
2 inss1 3389 . 2  |-  ( A  i^i  ( B  X.  _V ) )  C_  A
31, 2eqsstri 3208 1  |-  ( A  |`  B )  C_  A
Colors of variables: wff set class
Syntax hints:   _Vcvv 2788    i^i cin 3151    C_ wss 3152    X. cxp 4687    |` cres 4691
This theorem is referenced by:  relssres  4992  resexg  4994  iss  4998  relresfld  5199  relcoi1  5201  funres  5293  funres11  5320  funcnvres  5321  2elresin  5355  fssres  5408  foimacnv  5490  frxp  6225  fnwelem  6230  tposss  6235  dftpos4  6253  smores  6369  smores2  6371  tfrlem15  6408  fidomdm  7138  imafi  7148  marypha1lem  7186  hartogslem1  7257  r0weon  7640  ackbij2lem3  7867  axdc3lem2  8077  smobeth  8208  wunres  8353  vdwnnlem1  13042  odf1o2  14884  gsumzres  15194  gsumzaddlem  15203  gsumzadd  15204  gsum2d  15223  dprdfadd  15255  dprdres  15263  dprd2dlem1  15276  dprd2da  15277  opsrtoslem2  16226  cnrest  17013  txss12  17300  txbasval  17301  fmss  17641  tsmsres  17826  isngp2  18119  equivcau  18726  cmetss  18740  volf  18888  dvcnvrelem1  19364  tdeglem4  19446  pserdv  19805  dvlog  19998  dchrelbas2  20476  issubgoi  20977  hlimadd  21772  hlimcaui  21816  hhsst  21843  hhsssh2  21847  hhsscms  21856  occllem  21882  nlelchi  22641  hmopidmchi  22731  umgrares  23287  nodenselem6  23751  funpartss  23893  residcp  24489  svs2  24899  svs3  24900  brresi  25795  bnd2lem  25927  diophrw  26250  dnnumch2  26554  lmhmlnmsplit  26597  lindfres  26705  hbtlem6  26745  symgsssg  26820  symgfisg  26821  psgnunilem5  26829  usgrares  27514
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ss 3166  df-res 4701
  Copyright terms: Public domain W3C validator