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

Theorem resss 4981
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 4703 . 2  |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
2 inss1 3391 . 2  |-  ( A  i^i  ( B  X.  _V ) )  C_  A
31, 2eqsstri 3210 1  |-  ( A  |`  B )  C_  A
Colors of variables: wff set class
Syntax hints:   _Vcvv 2790    i^i cin 3153    C_ wss 3154    X. cxp 4689    |` cres 4693
This theorem is referenced by:  relssres  4994  resexg  4996  iss  5000  relresfld  5201  relcoi1  5203  funres  5295  funres11  5322  funcnvres  5323  2elresin  5357  fssres  5410  foimacnv  5492  frxp  6227  fnwelem  6232  tposss  6237  dftpos4  6255  smores  6371  smores2  6373  tfrlem15  6410  fidomdm  7140  imafi  7150  marypha1lem  7188  hartogslem1  7259  r0weon  7642  ackbij2lem3  7869  axdc3lem2  8079  smobeth  8210  wunres  8355  vdwnnlem1  13044  odf1o2  14886  gsumzres  15196  gsumzaddlem  15205  gsumzadd  15206  gsum2d  15225  dprdfadd  15257  dprdres  15265  dprd2dlem1  15278  dprd2da  15279  opsrtoslem2  16228  cnrest  17015  txss12  17302  txbasval  17303  fmss  17643  tsmsres  17828  isngp2  18121  equivcau  18728  cmetss  18742  volf  18890  dvcnvrelem1  19366  tdeglem4  19448  pserdv  19807  dvlog  20000  dchrelbas2  20478  issubgoi  20979  hlimadd  21774  hlimcaui  21818  hhsst  21845  hhsssh2  21849  hhsscms  21858  occllem  21884  nlelchi  22643  hmopidmchi  22733  dmct  23344  umgrares  23878  nodenselem6  24342  funpartss  24484  residcp  25088  svs2  25498  svs3  25499  brresi  26394  bnd2lem  26526  diophrw  26849  dnnumch2  27153  lmhmlnmsplit  27196  lindfres  27304  hbtlem6  27344  symgsssg  27419  symgfisg  27420  psgnunilem5  27428  usgrares  28126
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792  df-in 3161  df-ss 3168  df-res 4703
  Copyright terms: Public domain W3C validator