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

Theorem resss 4978
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 4700 . 2  |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
2 inss1 3390 . 2  |-  ( A  i^i  ( B  X.  _V ) )  C_  A
31, 2eqsstri 3209 1  |-  ( A  |`  B )  C_  A
Colors of variables: wff set class
Syntax hints:   _Vcvv 2789    i^i cin 3152    C_ wss 3153    X. cxp 4686    |` cres 4690
This theorem is referenced by:  relssres  4991  resexg  4993  iss  4997  relresfld  5197  relcoi1  5199  funres  5259  funres11  5286  funcnvres  5287  2elresin  5321  fssres  5374  foimacnv  5456  frxp  6187  fnwelem  6192  tposss  6197  dftpos4  6215  smores  6365  smores2  6367  tfrlem15  6404  fidomdm  7134  imafi  7144  marypha1lem  7182  hartogslem1  7253  r0weon  7636  ackbij2lem3  7863  axdc3lem2  8073  smobeth  8204  wunres  8349  vdwnnlem1  13038  odf1o2  14880  gsumzres  15190  gsumzaddlem  15199  gsumzadd  15200  gsum2d  15219  dprdfadd  15251  dprdres  15259  dprd2dlem1  15272  dprd2da  15273  opsrtoslem2  16222  cnrest  17009  txss12  17296  txbasval  17297  fmss  17637  tsmsres  17822  isngp2  18115  equivcau  18722  cmetss  18736  volf  18884  dvcnvrelem1  19360  tdeglem4  19442  pserdv  19801  dvlog  19994  dchrelbas2  20472  issubgoi  20971  hlimadd  21768  hlimcaui  21812  hhsst  21839  hhsssh2  21843  hhsscms  21852  occllem  21878  nlelchi  22637  hmopidmchi  22727  umgrares  23283  axdenselem6  23744  funpartss  23892  residcp  24487  svs2  24898  svs3  24899  brresi  25794  bnd2lem  25926  diophrw  26249  dnnumch2  26553  lmhmlnmsplit  26596  lindfres  26704  hbtlem6  26744  symgsssg  26819  symgfisg  26820  psgnunilem5  26828
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-in 3160  df-ss 3167  df-res 4700
  Copyright terms: Public domain W3C validator