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

Theorem resss 5325
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 5036 . 2 (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
2 inss1 3790 . 2 (𝐴 ∩ (𝐵 × V)) ⊆ 𝐴
31, 2eqsstri 3593 1 (𝐴𝐵) ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  Vcvv 3168  cin 3534  wss 3535   × cxp 5022  cres 5026
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-v 3170  df-in 3542  df-ss 3549  df-res 5036
This theorem is referenced by:  relssres  5340  resexg  5345  iss  5350  mptss  5356  relresfld  5561  funres  5825  funres11  5862  funcnvres  5863  2elresin  5898  fssres  5964  foimacnv  6048  frxp  7147  fnwelem  7152  tposss  7213  dftpos4  7231  smores  7309  smores2  7311  tfrlem15  7348  finresfin  8044  fidomdm  8101  imafi  8115  marypha1lem  8195  hartogslem1  8303  r0weon  8691  ackbij2lem3  8919  axdc3lem2  9129  smobeth  9260  wunres  9405  vdwnnlem1  15479  symgsssg  17652  symgfisg  17653  psgnunilem5  17679  odf1o2  17753  gsumzres  18075  gsumzaddlem  18086  gsumzadd  18087  gsum2dlem2  18135  dprdfadd  18184  dprdres  18192  dprd2dlem1  18205  dprd2da  18206  opsrtoslem2  19248  lindfres  19919  txss12  21156  txbasval  21157  fmss  21498  ustneism  21775  trust  21781  isngp2  22148  equivcau  22820  cmetss  22834  volf  23017  dvcnvrelem1  23497  tdeglem4  23537  pserdv  23900  dvlog  24110  dchrelbas2  24675  uhgrares  25599  umgrares  25615  usgrares  25660  hlimadd  27236  hlimcaui  27279  hhssabloilem  27304  hhsst  27309  hhsssh2  27313  hhsscms  27322  occllem  27348  nlelchi  28106  hmopidmchi  28196  fnresin  28614  imafi2  28674  dmct  28679  omsmon  29489  carsggect  29509  eulerpartlemmf  29566  nodenselem6  30887  funpartss  31023  brresi  32482  bnd2lem  32559  diophrw  36139  dnnumch2  36432  lmhmlnmsplit  36474  hbtlem6  36517  dfrcl2  36784  relexpaddss  36828  cotrclrcl  36852  frege131d  36874  rnresss  38159  fourierdlem42  38842  fourierdlem80  38879  resisresindm  40131  issubgr2  40494  subgrprop2  40496  uhgrspansubgr  40513
  Copyright terms: Public domain W3C validator