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

Theorem resss 4967
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 4681 . 2  |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
2 inss1 3364 . 2  |-  ( A  i^i  ( B  X.  _V ) )  C_  A
31, 2eqsstri 3183 1  |-  ( A  |`  B )  C_  A
Colors of variables: wff set class
Syntax hints:   _Vcvv 2763    i^i cin 3126    C_ wss 3127    X. cxp 4659    |` cres 4663
This theorem is referenced by:  relssres  4980  resexg  4982  iss  4986  relresfld  5186  relcoi1  5188  funres  5231  funres11  5258  funcnvres  5259  2elresin  5293  fssres  5346  foimacnv  5428  frxp  6159  fnwelem  6164  tposss  6169  dftpos4  6187  smores  6337  smores2  6339  tfrlem15  6376  fidomdm  7106  imafi  7116  marypha1lem  7154  hartogslem1  7225  r0weon  7608  ackbij2lem3  7835  axdc3lem2  8045  smobeth  8176  wunres  8321  vdwnnlem1  13005  odf1o2  14847  gsumzres  15157  gsumzaddlem  15166  gsumzadd  15167  gsum2d  15186  dprdfadd  15218  dprdres  15226  dprd2dlem1  15239  dprd2da  15240  opsrtoslem2  16189  cnrest  16976  txss12  17263  txbasval  17264  fmss  17604  tsmsres  17789  isngp2  18082  equivcau  18689  cmetss  18703  volf  18851  dvcnvrelem1  19327  tdeglem4  19409  pserdv  19768  dvlog  19961  dchrelbas2  20439  issubgoi  20938  hlimadd  21733  hlimcaui  21777  hhsst  21804  hhsssh2  21808  hhsscms  21817  occllem  21843  nlelchi  22602  hmopidmchi  22692  umgrares  23249  axdenselem6  23710  funpartss  23858  residcp  24444  svs2  24855  svs3  24856  brresi  25751  bnd2lem  25883  diophrw  26206  dnnumch2  26510  lmhmlnmsplit  26553  lindfres  26661  hbtlem6  26701  symgsssg  26776  symgfisg  26777  psgnunilem5  26785
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-v 2765  df-in 3134  df-ss 3141  df-res 4681
  Copyright terms: Public domain W3C validator