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

Theorem resss 4995
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 4717 . 2  |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
2 inss1 3402 . 2  |-  ( A  i^i  ( B  X.  _V ) )  C_  A
31, 2eqsstri 3221 1  |-  ( A  |`  B )  C_  A
Colors of variables: wff set class
Syntax hints:   _Vcvv 2801    i^i cin 3164    C_ wss 3165    X. cxp 4703    |` cres 4707
This theorem is referenced by:  relssres  5008  resexg  5010  iss  5014  relresfld  5215  relcoi1  5217  funres  5309  funres11  5336  funcnvres  5337  2elresin  5371  fssres  5424  foimacnv  5506  frxp  6241  fnwelem  6246  tposss  6251  dftpos4  6269  smores  6385  smores2  6387  tfrlem15  6424  fidomdm  7154  imafi  7164  marypha1lem  7202  hartogslem1  7273  r0weon  7656  ackbij2lem3  7883  axdc3lem2  8093  smobeth  8224  wunres  8369  vdwnnlem1  13058  odf1o2  14900  gsumzres  15210  gsumzaddlem  15219  gsumzadd  15220  gsum2d  15239  dprdfadd  15271  dprdres  15279  dprd2dlem1  15292  dprd2da  15293  opsrtoslem2  16242  cnrest  17029  txss12  17316  txbasval  17317  fmss  17657  tsmsres  17842  isngp2  18135  equivcau  18742  cmetss  18756  volf  18904  dvcnvrelem1  19380  tdeglem4  19462  pserdv  19821  dvlog  20014  dchrelbas2  20492  issubgoi  20993  hlimadd  21788  hlimcaui  21832  hhsst  21859  hhsssh2  21863  hhsscms  21872  occllem  21898  nlelchi  22657  hmopidmchi  22747  dmct  23357  umgrares  23891  nodenselem6  24411  funpartss  24554  residcp  25180  svs2  25590  svs3  25591  brresi  26486  bnd2lem  26618  diophrw  26941  dnnumch2  27245  lmhmlnmsplit  27288  lindfres  27396  hbtlem6  27436  symgsssg  27511  symgfisg  27512  psgnunilem5  27520  usgrares  28249
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-ss 3179  df-res 4717
  Copyright terms: Public domain W3C validator