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

Theorem resss 5110
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 4830 . 2  |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
2 inss1 3504 . 2  |-  ( A  i^i  ( B  X.  _V ) )  C_  A
31, 2eqsstri 3321 1  |-  ( A  |`  B )  C_  A
Colors of variables: wff set class
Syntax hints:   _Vcvv 2899    i^i cin 3262    C_ wss 3263    X. cxp 4816    |` cres 4820
This theorem is referenced by:  relssres  5123  resexg  5125  iss  5129  relresfld  5336  relcoi1  5338  funres  5432  funres11  5461  funcnvres  5462  2elresin  5496  fssres  5550  foimacnv  5632  frxp  6392  fnwelem  6397  tposss  6416  dftpos4  6434  smores  6550  smores2  6552  tfrlem15  6589  finresfin  7270  fidomdm  7324  imafi  7334  marypha1lem  7373  hartogslem1  7444  r0weon  7827  ackbij2lem3  8054  axdc3lem2  8264  smobeth  8394  wunres  8539  vdwnnlem1  13290  odf1o2  15134  gsumzres  15444  gsumzaddlem  15453  gsumzadd  15454  gsum2d  15473  dprdfadd  15505  dprdres  15513  dprd2dlem1  15526  dprd2da  15527  opsrtoslem2  16472  cnrest  17271  txss12  17558  txbasval  17559  fmss  17899  tsmsres  18094  ustneism  18174  trust  18180  isngp2  18515  equivcau  19124  cmetss  19138  volf  19292  dvcnvrelem1  19768  tdeglem4  19850  pserdv  20212  dvlog  20409  dchrelbas2  20888  uhgrares  21210  umgrares  21226  usgrares  21256  issubgoi  21746  hlimadd  22543  hlimcaui  22587  hhsst  22614  hhsssh2  22618  hhsscms  22627  occllem  22653  nlelchi  23412  hmopidmchi  23502  dmct  23947  nodenselem6  25364  funpartss  25507  brresi  26111  bnd2lem  26191  diophrw  26508  dnnumch2  26811  lmhmlnmsplit  26854  lindfres  26962  hbtlem6  27002  symgsssg  27077  symgfisg  27078  psgnunilem5  27086
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-v 2901  df-in 3270  df-ss 3277  df-res 4830
  Copyright terms: Public domain W3C validator