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

Theorem resss 5766
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 5462 . 2 (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
2 inss1 4131 . 2 (𝐴 ∩ (𝐵 × V)) ⊆ 𝐴
31, 2eqsstri 3928 1 (𝐴𝐵) ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  Vcvv 3440  cin 3864  wss 3865   × cxp 5448  cres 5452
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-v 3442  df-in 3872  df-ss 3880  df-res 5462
This theorem is referenced by:  relssres  5781  resexg  5786  iss  5791  mptss  5798  relresfld  6009  funres  6274  funres11  6308  funcnvres  6309  2elresin  6345  fssres  6419  foimacnv  6507  frxp  7680  fnwelem  7685  tposss  7751  dftpos4  7769  smores  7848  smores2  7850  tfrlem15  7887  finresfin  8597  fidomdm  8654  imafi  8670  marypha1lem  8750  hartogslem1  8859  r0weon  9291  ackbij2lem3  9516  axdc3lem2  9726  dmct  9799  smobeth  9861  wunres  10006  vdwnnlem1  16164  symgsssg  18330  symgfisg  18331  psgnunilem5  18357  odf1o2  18432  gsumzres  18754  gsumzaddlem  18765  gsumzadd  18766  gsum2dlem2  18815  dprdfadd  18863  dprdres  18871  dprd2dlem1  18884  dprd2da  18885  opsrtoslem2  19956  lindfres  20653  txss12  21901  txbasval  21902  fmss  22242  ustneism  22519  trust  22525  isngp2  22893  equivcau  23590  metsscmetcld  23605  volf  23817  dvcnvrelem1  24301  tdeglem4  24341  pserdv  24704  dvlog  24919  dchrelbas2  25499  issubgr2  26741  subgrprop2  26743  uhgrspansubgr  26760  hlimadd  28657  hlimcaui  28700  hhssabloilem  28725  hhsst  28730  hhsssh2  28734  hhsscms  28742  occllem  28767  nlelchi  29525  hmopidmchi  29615  fnresin  30057  imafi2  30131  omsmon  31169  carsggect  31189  eulerpartlemmf  31246  funpartss  33016  brresi2  34547  bnd2lem  34622  idresssidinxp  35119  disjimres  35532  diophrw  38862  dnnumch2  39151  lmhmlnmsplit  39193  hbtlem6  39235  dfrcl2  39525  relexpaddss  39569  cotrclrcl  39593  frege131d  39615  rnresss  41000  resimass  41072  fourierdlem42  41998  fourierdlem80  42035  setrecsres  44306
  Copyright terms: Public domain W3C validator