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

Theorem resss 4932
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 4646 . 2  |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
2 inss1 3331 . 2  |-  ( A  i^i  ( B  X.  _V ) )  C_  A
31, 2eqsstri 3150 1  |-  ( A  |`  B )  C_  A
Colors of variables: wff set class
Syntax hints:   _Vcvv 2740    i^i cin 3093    C_ wss 3094    X. cxp 4624    |` cres 4628
This theorem is referenced by:  relssres  4945  resexg  4947  iss  4951  relresfld  5151  relcoi1  5153  funres  5196  funres11  5223  funcnvres  5224  2elresin  5258  fssres  5311  foimacnv  5393  frxp  6124  fnwelem  6129  tposss  6134  dftpos4  6152  smores  6302  smores2  6304  tfrlem15  6341  fidomdm  7071  imafi  7081  marypha1lem  7119  hartogslem1  7190  r0weon  7573  ackbij2lem3  7800  axdc3lem2  8010  smobeth  8141  wunres  8286  vdwnnlem1  12969  odf1o2  14811  gsumzres  15121  gsumzaddlem  15130  gsumzadd  15131  gsum2d  15150  dprdfadd  15182  dprdres  15190  dprd2dlem1  15203  dprd2da  15204  opsrtoslem2  16153  cnrest  16940  txss12  17227  txbasval  17228  fmss  17568  tsmsres  17753  isngp2  18046  equivcau  18653  cmetss  18667  volf  18815  dvcnvrelem1  19291  tdeglem4  19373  pserdv  19732  dvlog  19925  dchrelbas2  20403  issubgoi  20902  hlimadd  21697  hlimcaui  21741  hhsst  21768  hhsssh2  21772  hhsscms  21781  occllem  21807  nlelchi  22566  hmopidmchi  22656  umgrares  23213  axdenselem6  23674  funpartss  23822  residcp  24408  svs2  24819  svs3  24820  brresi  25715  bnd2lem  25847  diophrw  26170  dnnumch2  26474  lmhmlnmsplit  26517  lindfres  26625  hbtlem6  26665  symgsssg  26740  symgfisg  26741  psgnunilem5  26749
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 2237
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 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2742  df-in 3101  df-ss 3108  df-res 4646
  Copyright terms: Public domain W3C validator