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

Theorem resss 5128
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 4846 . 2  |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
2 inss1 3652 . 2  |-  ( A  i^i  ( B  X.  _V ) )  C_  A
31, 2eqsstri 3462 1  |-  ( A  |`  B )  C_  A
Colors of variables: wff setvar class
Syntax hints:   _Vcvv 3045    i^i cin 3403    C_ wss 3404    X. cxp 4832    |` cres 4836
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-v 3047  df-in 3411  df-ss 3418  df-res 4846
This theorem is referenced by:  relssres  5142  resexg  5147  iss  5152  relresfld  5362  relcoi1OLD  5365  funres  5621  funres11  5651  funcnvres  5652  2elresin  5687  fssres  5749  foimacnv  5831  frxp  6906  fnwelem  6911  tposss  6974  dftpos4  6992  smores  7071  smores2  7073  tfrlem15  7110  finresfin  7797  fidomdm  7853  imafi  7867  marypha1lem  7947  hartogslem1  8057  r0weon  8443  ackbij2lem3  8671  axdc3lem2  8881  smobeth  9011  wunres  9156  vdwnnlem1  14945  symgsssg  17108  symgfisg  17109  psgnunilem5  17135  odf1o2  17222  gsumzres  17543  gsumzaddlem  17554  gsumzadd  17555  gsum2dlem2  17603  dprdfadd  17653  dprdres  17661  dprd2dlem1  17674  dprd2da  17675  opsrtoslem2  18708  lindfres  19381  txss12  20620  txbasval  20621  fmss  20961  ustneism  21238  trust  21244  isngp2  21611  equivcau  22270  cmetss  22284  volf  22483  dvcnvrelem1  22969  tdeglem4  23009  pserdv  23384  dvlog  23596  dchrelbas2  24165  uhgrares  25035  umgrares  25051  usgrares  25096  issubgoi  26038  hlimadd  26846  hlimcaui  26889  hhsst  26917  hhsssh2  26921  hhsscms  26930  occllem  26956  nlelchi  27714  hmopidmchi  27804  fnresin  28228  imafi2  28292  dmct  28298  omsmon  29126  omsmonOLD  29130  carsggect  29150  eulerpartlemmf  29208  nodenselem6  30575  funpartss  30711  brresi  32045  bnd2lem  32123  diophrw  35601  dnnumch2  35903  lmhmlnmsplit  35945  hbtlem6  35988  dfrcl2  36266  relexpaddss  36310  cotrclrcl  36334  frege131d  36356  rnresss  37451  mptss  37455  fourierdlem42  38012  fourierdlem42OLD  38013  fourierdlem80  38050  resisresindm  39011  issubgr2  39344  subgrprop2  39346  uhgrspansubgr  39363  uhgres  39744
  Copyright terms: Public domain W3C validator