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

Theorem resss 5872
Description: A class includes its restriction. Exercise 15 of [TakeutiZaring] p. 25. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
resss (𝐴𝐵) ⊆ 𝐴

Proof of Theorem resss
StepHypRef Expression
1 df-res 5561 . 2 (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
2 inss1 4204 . 2 (𝐴 ∩ (𝐵 × V)) ⊆ 𝐴
31, 2eqsstri 4000 1 (𝐴𝐵) ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  Vcvv 3495  cin 3934  wss 3935   × cxp 5547  cres 5551
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3497  df-in 3942  df-ss 3951  df-res 5561
This theorem is referenced by:  relssres  5887  resexg  5892  iss  5897  mptss  5904  relresfld  6121  funres  6391  funres11  6425  funcnvres  6426  2elresin  6462  fssres  6538  foimacnv  6626  frxp  7811  fnwelem  7816  tposss  7884  dftpos4  7902  smores  7980  smores2  7982  tfrlem15  8019  finresfin  8733  fidomdm  8790  imafi  8806  marypha1lem  8886  hartogslem1  8995  r0weon  9427  ackbij2lem3  9652  axdc3lem2  9862  dmct  9935  smobeth  9997  wunres  10142  vdwnnlem1  16321  symgsssg  18526  symgfisg  18527  psgnunilem5  18553  odf1o2  18629  gsumzres  18960  gsumzaddlem  18972  gsumzadd  18973  gsum2dlem2  19022  dprdfadd  19073  dprdres  19081  dprd2dlem1  19094  dprd2da  19095  opsrtoslem2  20195  lindfres  20897  txss12  22143  txbasval  22144  fmss  22484  ustneism  22761  trust  22767  isngp2  23135  equivcau  23832  metsscmetcld  23847  volf  24059  dvcnvrelem1  24543  tdeglem4  24583  pserdv  24946  dvlog  25161  dchrelbas2  25741  issubgr2  26982  subgrprop2  26984  uhgrspansubgr  27001  hlimadd  28898  hlimcaui  28941  hhssabloilem  28966  hhsst  28971  hhsssh2  28975  hhsscms  28983  occllem  29008  nlelchi  29766  hmopidmchi  29856  fnresin  30300  imafi2  30374  pfxrn2  30544  omsmon  31456  carsggect  31476  eulerpartlemmf  31533  funpartss  33303  brresi2  34877  bnd2lem  34952  idresssidinxp  35449  disjimres  35862  diophrw  39236  dnnumch2  39525  lmhmlnmsplit  39567  hbtlem6  39609  dfrcl2  39899  relexpaddss  39943  cotrclrcl  39967  frege131d  39989  rnresss  41319  resimass  41390  fourierdlem42  42315  fourierdlem80  42352  setrecsres  44702
  Copyright terms: Public domain W3C validator