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

Theorem resss 5871
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 5560 . 2 (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
2 inss1 4202 . 2 (𝐴 ∩ (𝐵 × V)) ⊆ 𝐴
31, 2eqsstri 3998 1 (𝐴𝐵) ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  Vcvv 3492  cin 3932  wss 3933   × cxp 5546  cres 5550
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 2790
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 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-in 3940  df-ss 3949  df-res 5560
This theorem is referenced by:  relssres  5886  resexg  5891  iss  5896  mptss  5903  relresfld  6120  funres  6390  funres11  6424  funcnvres  6425  2elresin  6461  fssres  6537  foimacnv  6625  frxp  7809  fnwelem  7814  tposss  7882  dftpos4  7900  smores  7978  smores2  7980  tfrlem15  8017  finresfin  8732  fidomdm  8789  imafi  8805  marypha1lem  8885  hartogslem1  8994  r0weon  9426  ackbij2lem3  9651  axdc3lem2  9861  dmct  9934  smobeth  9996  wunres  10141  vdwnnlem1  16319  symgsssg  18524  symgfisg  18525  psgnunilem5  18551  odf1o2  18627  gsumzres  18958  gsumzaddlem  18970  gsumzadd  18971  gsum2dlem2  19020  dprdfadd  19071  dprdres  19079  dprd2dlem1  19092  dprd2da  19093  opsrtoslem2  20193  lindfres  20895  txss12  22141  txbasval  22142  fmss  22482  ustneism  22759  trust  22765  isngp2  23133  equivcau  23830  metsscmetcld  23845  volf  24057  dvcnvrelem1  24541  tdeglem4  24581  pserdv  24944  dvlog  25161  dchrelbas2  25740  issubgr2  26981  subgrprop2  26983  uhgrspansubgr  27000  hlimadd  28897  hlimcaui  28940  hhssabloilem  28965  hhsst  28970  hhsssh2  28974  hhsscms  28982  occllem  29007  nlelchi  29765  hmopidmchi  29855  fnresin  30299  imafi2  30373  pfxrn2  30543  omsmon  31455  carsggect  31475  eulerpartlemmf  31532  funpartss  33302  brresi2  34875  bnd2lem  34950  idresssidinxp  35447  disjimres  35860  diophrw  39234  dnnumch2  39523  lmhmlnmsplit  39565  hbtlem6  39607  dfrcl2  39897  relexpaddss  39941  cotrclrcl  39965  frege131d  39987  rnresss  41315  resimass  41386  fourierdlem42  42311  fourierdlem80  42348  setrecsres  44732
  Copyright terms: Public domain W3C validator