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

Theorem resss 5139
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 4857 . 2  |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
2 inss1 3679 . 2  |-  ( A  i^i  ( B  X.  _V ) )  C_  A
31, 2eqsstri 3491 1  |-  ( A  |`  B )  C_  A
Colors of variables: wff setvar class
Syntax hints:   _Vcvv 3078    i^i cin 3432    C_ wss 3433    X. cxp 4843    |` cres 4847
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-v 3080  df-in 3440  df-ss 3447  df-res 4857
This theorem is referenced by:  relssres  5153  resexg  5158  iss  5163  relresfld  5373  relcoi1OLD  5376  funres  5631  funres11  5660  funcnvres  5661  2elresin  5696  fssres  5757  foimacnv  5839  frxp  6908  fnwelem  6913  tposss  6973  dftpos4  6991  smores  7070  smores2  7072  tfrlem15  7109  finresfin  7794  fidomdm  7850  imafi  7864  marypha1lem  7944  hartogslem1  8048  r0weon  8433  ackbij2lem3  8660  axdc3lem2  8870  smobeth  9000  wunres  9145  vdwnnlem1  14897  symgsssg  17052  symgfisg  17053  psgnunilem5  17079  odf1o2  17153  gsumzres  17471  gsumzaddlem  17482  gsumzadd  17483  gsum2dlem2  17531  dprdfadd  17581  dprdres  17589  dprd2dlem1  17602  dprd2da  17603  opsrtoslem2  18636  lindfres  19305  txss12  20544  txbasval  20545  fmss  20885  ustneism  21162  trust  21168  isngp2  21535  equivcau  22176  cmetss  22190  volf  22377  dvcnvrelem1  22863  tdeglem4  22903  pserdv  23275  dvlog  23487  dchrelbas2  24054  uhgrares  24907  umgrares  24923  usgrares  24968  issubgoi  25909  hlimadd  26707  hlimcaui  26750  hhsst  26778  hhsssh2  26782  hhsscms  26791  occllem  26817  nlelchi  27575  hmopidmchi  27665  fnresin  28094  imafi2  28157  dmct  28167  omsmon  28985  carsggect  29005  eulerpartlemmf  29060  nodenselem6  30386  funpartss  30522  brresi  31778  bnd2lem  31856  diophrw  35339  dnnumch2  35642  lmhmlnmsplit  35684  hbtlem6  35727  dfrcl2  35938  relexpaddss  35982  cotrclrcl  36006  frege131d  36028  rnresss  37107  mptss  37111  fourierdlem42  37613  fourierdlem80  37651  resisresindm  38424  uhgres  38491
  Copyright terms: Public domain W3C validator