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

Theorem resss 4886
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 4600 . 2  |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
2 inss1 3296 . 2  |-  ( A  i^i  ( B  X.  _V ) )  C_  A
31, 2eqsstri 3129 1  |-  ( A  |`  B )  C_  A
Colors of variables: wff set class
Syntax hints:   _Vcvv 2727    i^i cin 3077    C_ wss 3078    X. cxp 4578    |` cres 4582
This theorem is referenced by:  relssres  4899  resexg  4901  iss  4905  relresfld  5105  relcoi1  5107  funres  5150  funres11  5177  funcnvres  5178  2elresin  5212  fssres  5265  foimacnv  5347  frxp  6077  fnwelem  6082  tposss  6087  dftpos4  6105  smores  6255  smores2  6257  tfrlem15  6294  fidomdm  7023  imafi  7032  marypha1lem  7070  hartogslem1  7141  r0weon  7524  ackbij2lem3  7751  axdc3lem2  7961  smobeth  8088  wunres  8233  vdwnnlem1  12916  odf1o2  14719  gsumzres  15029  gsumzaddlem  15038  gsumzadd  15039  gsum2d  15058  dprdfadd  15090  dprdres  15098  dprd2dlem1  15111  dprd2da  15112  opsrtoslem2  16058  cnrest  16845  txss12  17132  txbasval  17133  fmss  17473  tsmsres  17658  isngp2  17951  equivcau  18558  cmetss  18572  volf  18720  dvcnvrelem1  19196  tdeglem4  19278  pserdv  19637  dvlog  19830  dchrelbas2  20308  issubgoi  20807  hlimadd  21602  hlimcaui  21646  hhsst  21673  hhsssh2  21677  hhsscms  21686  occllem  21712  nlelchi  22471  hmopidmchi  22561  umgrares  23047  axdenselem6  23508  funpartss  23656  residcp  24242  svs2  24653  svs3  24654  brresi  25549  bnd2lem  25681  diophrw  26004  dnnumch2  26308  lmhmlnmsplit  26351  lindfres  26459  hbtlem6  26499  symgsssg  26574  symgfisg  26575  psgnunilem5  26583
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-in 3085  df-ss 3089  df-res 4600
  Copyright terms: Public domain W3C validator