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

Theorem resss 5162
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 4882 . 2  |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
2 inss1 3553 . 2  |-  ( A  i^i  ( B  X.  _V ) )  C_  A
31, 2eqsstri 3370 1  |-  ( A  |`  B )  C_  A
Colors of variables: wff set class
Syntax hints:   _Vcvv 2948    i^i cin 3311    C_ wss 3312    X. cxp 4868    |` cres 4872
This theorem is referenced by:  relssres  5175  resexg  5177  iss  5181  relresfld  5388  relcoi1  5390  funres  5484  funres11  5513  funcnvres  5514  2elresin  5548  fssres  5602  foimacnv  5684  frxp  6448  fnwelem  6453  tposss  6472  dftpos4  6490  smores  6606  smores2  6608  tfrlem15  6645  finresfin  7326  fidomdm  7380  imafi  7391  marypha1lem  7430  hartogslem1  7503  r0weon  7886  ackbij2lem3  8113  axdc3lem2  8323  smobeth  8453  wunres  8598  vdwnnlem1  13355  odf1o2  15199  gsumzres  15509  gsumzaddlem  15518  gsumzadd  15519  gsum2d  15538  dprdfadd  15570  dprdres  15578  dprd2dlem1  15591  dprd2da  15592  opsrtoslem2  16537  cnrest  17341  txss12  17629  txbasval  17630  fmss  17970  tsmsres  18165  ustneism  18245  trust  18251  isngp2  18636  equivcau  19245  cmetss  19259  volf  19417  dvcnvrelem1  19893  tdeglem4  19975  pserdv  20337  dvlog  20534  dchrelbas2  21013  uhgrares  21335  umgrares  21351  usgrares  21381  issubgoi  21890  hlimadd  22687  hlimcaui  22731  hhsst  22758  hhsssh2  22762  hhsscms  22771  occllem  22797  nlelchi  23556  hmopidmchi  23646  dmct  24098  nodenselem6  25633  funpartss  25781  brresi  26411  bnd2lem  26491  diophrw  26808  dnnumch2  27111  lmhmlnmsplit  27153  lindfres  27261  hbtlem6  27301  symgsssg  27376  symgfisg  27377  psgnunilem5  27385  resisresindm  28061
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-in 3319  df-ss 3326  df-res 4882
  Copyright terms: Public domain W3C validator