Theorem resss 5961

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 5643	. 2 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		inss1 4196	. 2 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ 𝐴
3	1, 2	eqsstri 3990	1 ⊢ (𝐴 ↾ 𝐵) ⊆ 𝐴

Syntax hints:  Vcvv 3444   ∩ cin 3910   ⊆ wss 3911   × cxp 5629   ↾ cres 5633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-in 3918  df-ss 3928  df-res 5643

This theorem is referenced by:  dmresss  5971  rnresss  5977  relssres  5982  resexg  5987  iss  5995  mptss  6002  relresfld  6237  funres  6542  funres11  6577  funcnvres  6578  2elresin  6621  fssres  6708  foimacnv  6799  frxp  8082  fnwelem  8087  tposss  8183  dftpos4  8201  smores  8298  smores2  8300  tfrlem15  8337  finresfin  9191  imafi  9240  fidomdm  9261  marypha1lem  9360  hartogslem1  9471  r0weon  9941  ackbij2lem3  10169  axdc3lem2  10380  dmct  10453  smobeth  10515  wunres  10660  vdwnnlem1  16942  symgsssg  19381  symgfisg  19382  psgnunilem5  19408  odf1o2  19487  gsumzres  19823  gsumzaddlem  19835  gsumzadd  19836  gsum2dlem2  19885  dprdfadd  19936  dprdres  19944  dprd2dlem1  19957  dprd2da  19958  lindfres  21765  opsrtoslem2  21996  txss12  23525  txbasval  23526  fmss  23866  ustneism  24144  trust  24150  isngp2  24518  equivcau  25233  metsscmetcld  25248  volf  25463  dvcnvrelem1  25955  pserdv  26372  dvlog  26593  dchrelbas2  27181  issubgr2  29252  subgrprop2  29254  uhgrspansubgr  29271  hlimadd  31172  hlimcaui  31215  hhssabloilem  31240  hhsst  31245  hhsssh2  31249  hhsscms  31257  occllem  31282  nlelchi  32040  hmopidmchi  32130  fnresin  32600  fressupp  32661  imafi2  32685  pfxrn2  32911  omsmon  34282  carsggect  34302  eulerpartlemmf  34359  funpartss  35925  brresi2  37707  bnd2lem  37778  idresssidinxp  38289  disjimres  38735  aks6d1c2  42111  eqresfnbd  42213  diophrw  42740  dnnumch2  43027  lmhmlnmsplit  43069  hbtlem6  43111  dfrcl2  43656  relexpaddss  43700  cotrclrcl  43724  frege131d  43746  resimass  45227  fourierdlem42  46140  fourierdlem80  46177  isubgredgss  47858  isubgrsubgr  47862  setrecsres  49684