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

Theorem resss 5297
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 5011 . 2  |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
2 inss1 3718 . 2  |-  ( A  i^i  ( B  X.  _V ) )  C_  A
31, 2eqsstri 3534 1  |-  ( A  |`  B )  C_  A
Colors of variables: wff setvar class
Syntax hints:   _Vcvv 3113    i^i cin 3475    C_ wss 3476    X. cxp 4997    |` cres 5001
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483  df-ss 3490  df-res 5011
This theorem is referenced by:  relssres  5311  resexg  5316  iss  5321  relresfld  5534  relcoi1  5536  funres  5627  funres11  5656  funcnvres  5657  2elresin  5692  fssres  5751  foimacnv  5833  frxp  6893  fnwelem  6898  tposss  6956  dftpos4  6974  smores  7023  smores2  7025  tfrlem15  7061  finresfin  7745  fidomdm  7802  imafi  7813  marypha1lem  7893  hartogslem1  7967  r0weon  8390  ackbij2lem3  8621  axdc3lem2  8831  smobeth  8961  wunres  9109  vdwnnlem1  14372  symgsssg  16298  symgfisg  16299  psgnunilem5  16325  odf1o2  16399  gsumzres  16717  gsumzresOLD  16721  gsumzaddlem  16737  gsumzadd  16738  gsumzaddlemOLD  16739  gsumzaddOLD  16740  gsum2dlem2  16801  gsum2dOLD  16803  dprdfadd  16862  dprdfaddOLD  16869  dprdres  16877  dprd2dlem1  16892  dprd2da  16893  opsrtoslem2  17948  lindfres  18653  cnrest  19580  txss12  19869  txbasval  19870  fmss  20210  tsmsresOLD  20408  ustneism  20489  trust  20495  isngp2  20880  equivcau  21502  cmetss  21516  volf  21703  dvcnvrelem1  22181  tdeglem4  22221  pserdv  22586  dvlog  22788  dchrelbas2  23268  uhgrares  24012  umgrares  24028  usgrares  24073  issubgoi  25016  hlimadd  25814  hlimcaui  25858  hhsst  25886  hhsssh2  25890  hhsscms  25899  occllem  25925  nlelchi  26684  hmopidmchi  26774  fnresin  27171  dmct  27237  omsmon  27935  eulerpartlemmf  27982  nodenselem6  29051  funpartss  29199  brresi  29840  bnd2lem  29918  diophrw  30324  dnnumch2  30623  lmhmlnmsplit  30665  hbtlem6  30710  fourierdlem42  31477  fourierdlem80  31515  resisresindm  31800  uhgres  31874
  Copyright terms: Public domain W3C validator