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

Theorem resss 5155
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 4873 . 2  |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
2 inss1 3591 . 2  |-  ( A  i^i  ( B  X.  _V ) )  C_  A
31, 2eqsstri 3407 1  |-  ( A  |`  B )  C_  A
Colors of variables: wff setvar class
Syntax hints:   _Vcvv 2993    i^i cin 3348    C_ wss 3349    X. cxp 4859    |` cres 4863
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2995  df-in 3356  df-ss 3363  df-res 4873
This theorem is referenced by:  relssres  5168  resexg  5170  iss  5175  relresfld  5385  relcoi1  5387  funres  5478  funres11  5507  funcnvres  5508  2elresin  5543  fssres  5599  foimacnv  5679  frxp  6703  fnwelem  6708  tposss  6767  dftpos4  6785  smores  6834  smores2  6836  tfrlem15  6872  finresfin  7559  fidomdm  7614  imafi  7625  marypha1lem  7704  hartogslem1  7777  r0weon  8200  ackbij2lem3  8431  axdc3lem2  8641  smobeth  8771  wunres  8919  vdwnnlem1  14077  symgsssg  15994  symgfisg  15995  psgnunilem5  16021  odf1o2  16093  gsumzres  16409  gsumzresOLD  16413  gsumzaddlem  16429  gsumzadd  16430  gsumzaddlemOLD  16431  gsumzaddOLD  16432  gsum2dlem2  16484  gsum2dOLD  16486  dprdfadd  16532  dprdfaddOLD  16539  dprdres  16547  dprd2dlem1  16562  dprd2da  16563  opsrtoslem2  17588  lindfres  18274  cnrest  18911  txss12  19200  txbasval  19201  fmss  19541  tsmsresOLD  19739  ustneism  19820  trust  19826  isngp2  20211  equivcau  20833  cmetss  20847  volf  21034  dvcnvrelem1  21511  tdeglem4  21551  pserdv  21916  dvlog  22118  dchrelbas2  22598  uhgrares  23264  umgrares  23280  usgrares  23310  issubgoi  23819  hlimadd  24617  hlimcaui  24661  hhsst  24689  hhsssh2  24693  hhsscms  24702  occllem  24728  nlelchi  25487  hmopidmchi  25577  fnresin  25969  dmct  26036  omsmon  26733  eulerpartlemmf  26780  nodenselem6  27849  funpartss  27997  brresi  28638  bnd2lem  28716  diophrw  29123  dnnumch2  29424  lmhmlnmsplit  29466  hbtlem6  29511  resisresindm  30165
  Copyright terms: Public domain W3C validator