Theorem resss 6001

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

Step	Hyp	Ref	Expression
1		df-res 5674	. 2 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		inss1 4197	. 2 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ 𝐴
3	1, 2	eqsstri 3991	1 ⊢ (𝐴 ↾ 𝐵) ⊆ 𝐴

Syntax hints:  Vcvv 3463   ∩ cin 3912   ⊆ wss 3913   × cxp 5660   ↾ cres 5664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-in 3920  df-ss 3930  df-res 5674

This theorem is referenced by:  dmresss  6011  rnresss  6017  relssres  6022  resexg  6027  iss  6038  mptss  6045  cnvcnvss  6193  relresfld  6278  funres  6579  funres11  6614  funcnvres  6615  2elresin  6657  fssres  6745  foimacnv  6839  frxp  8122  fnwelem  8127  tposss  8223  dftpos4  8241  smores  8339  smores2  8341  tfrlem15  8379  finresfin  9232  imafi  9275  fidomdm  9291  imafi2  9318  marypha1lem  9393  hartogslem1  9504  r0weon  9996  ackbij2lem3  10223  axdc3lem2  10435  dmct  10508  smobeth  10571  wunres  10716  vdwnnlem1  17055  symgsssg  19537  symgfisg  19538  psgnunilem5  19564  odf1o2  19643  gsumzres  19979  gsumzaddlem  19991  gsumzadd  19992  gsum2dlem2  20041  dprdfadd  20092  dprdres  20100  dprd2dlem1  20113  dprd2da  20114  lindfres  21942  opsrtoslem2  22176  txss12  23731  txbasval  23732  fmss  24072  ustneism  24350  trust  24355  isngp2  24723  equivcau  25428  metsscmetcld  25443  volf  25657  dvcnvrelem1  26145  pserdv  26558  dvlog  26782  dchrelbas2  27367  issubgr2  29563  subgrprop2  29565  uhgrspansubgr  29582  hlimadd  31486  hlimcaui  31529  hhssabloilem  31554  hhsst  31559  hhsssh2  31563  hhsscms  31571  occllem  31596  nlelchi  32354  hmopidmchi  32444  fnresin  32910  fressupp  32974  pfxrn2  33201  omsmon  34633  carsggect  34653  eulerpartlemmf  34710  funpartss  36369  brresi2  38293  bnd2lem  38364  idresssidinxp  38887  disjimres  39423  aks6d1c2  42821  eqresfnbd  42927  diophrw  43416  dnnumch2  43698  lmhmlnmsplit  43740  hbtlem6  43782  dfrcl2  44326  relexpaddss  44370  cotrclrcl  44394  frege131d  44416  resimass  45881  fourierdlem42  46789  fourierdlem80  46826  isubgredgss  48553  isubgrsubgr  48557  setrecsres  50399