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

Theorem resss 5960
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 5643 . 2 (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
2 inss1 4186 . 2 (𝐴 ∩ (𝐵 × V)) ⊆ 𝐴
31, 2eqsstri 3976 1 (𝐴𝐵) ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  Vcvv 3443  cin 3907  wss 3908   × cxp 5629  cres 5633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3445  df-in 3915  df-ss 3925  df-res 5643
This theorem is referenced by:  rnresss  5971  relssres  5976  resexg  5981  iss  5987  mptss  5994  relresfld  6226  funres  6540  funres11  6575  funcnvres  6576  2elresin  6619  fssres  6705  foimacnv  6798  frxp  8050  fnwelem  8055  tposss  8150  dftpos4  8168  smores  8290  smores2  8292  tfrlem15  8330  finresfin  9172  fidomdm  9231  imafiALT  9247  marypha1lem  9327  hartogslem1  9436  r0weon  9906  ackbij2lem3  10135  axdc3lem2  10345  dmct  10418  smobeth  10480  wunres  10625  vdwnnlem1  16827  symgsssg  19208  symgfisg  19209  psgnunilem5  19235  odf1o2  19314  gsumzres  19645  gsumzaddlem  19657  gsumzadd  19658  gsum2dlem2  19707  dprdfadd  19758  dprdres  19766  dprd2dlem1  19779  dprd2da  19780  lindfres  21182  opsrtoslem2  21415  txss12  22908  txbasval  22909  fmss  23249  ustneism  23527  trust  23533  isngp2  23905  equivcau  24616  metsscmetcld  24631  volf  24845  dvcnvrelem1  25333  tdeglem4OLD  25377  pserdv  25740  dvlog  25958  dchrelbas2  26537  issubgr2  28049  subgrprop2  28051  uhgrspansubgr  28068  hlimadd  29964  hlimcaui  30007  hhssabloilem  30032  hhsst  30037  hhsssh2  30041  hhsscms  30049  occllem  30074  nlelchi  30832  hmopidmchi  30922  fnresin  31369  fressupp  31430  imafi2  31454  pfxrn2  31622  omsmon  32710  carsggect  32730  eulerpartlemmf  32787  funpartss  34467  brresi2  36116  bnd2lem  36188  idresssidinxp  36707  disjimres  37150  diophrw  40991  dnnumch2  41281  lmhmlnmsplit  41323  hbtlem6  41365  dfrcl2  41857  relexpaddss  41901  cotrclrcl  41925  frege131d  41947  resimass  43371  fourierdlem42  44291  fourierdlem80  44328  setrecsres  47048
  Copyright terms: Public domain W3C validator