Theorem resss 5960

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

Syntax hints:  Vcvv 3440   ∩ cin 3900   ⊆ wss 3901   × cxp 5622   ↾ cres 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-in 3908  df-ss 3918  df-res 5636

This theorem is referenced by:  dmresss  5970  rnresss  5976  relssres  5981  resexg  5986  iss  5994  mptss  6001  relresfld  6234  funres  6534  funres11  6569  funcnvres  6570  2elresin  6613  fssres  6700  foimacnv  6791  frxp  8068  fnwelem  8073  tposss  8169  dftpos4  8187  smores  8284  smores2  8286  tfrlem15  8323  finresfin  9174  imafi  9217  fidomdm  9236  imafi2  9263  marypha1lem  9338  hartogslem1  9449  r0weon  9924  ackbij2lem3  10152  axdc3lem2  10363  dmct  10436  smobeth  10499  wunres  10644  vdwnnlem1  16925  symgsssg  19398  symgfisg  19399  psgnunilem5  19425  odf1o2  19504  gsumzres  19840  gsumzaddlem  19852  gsumzadd  19853  gsum2dlem2  19902  dprdfadd  19953  dprdres  19961  dprd2dlem1  19974  dprd2da  19975  lindfres  21780  opsrtoslem2  22013  txss12  23551  txbasval  23552  fmss  23892  ustneism  24170  trust  24175  isngp2  24543  equivcau  25258  metsscmetcld  25273  volf  25488  dvcnvrelem1  25980  pserdv  26397  dvlog  26618  dchrelbas2  27206  issubgr2  29347  subgrprop2  29349  uhgrspansubgr  29366  hlimadd  31270  hlimcaui  31313  hhssabloilem  31338  hhsst  31343  hhsssh2  31347  hhsscms  31355  occllem  31380  nlelchi  32138  hmopidmchi  32228  fnresin  32704  fressupp  32769  pfxrn2  33024  omsmon  34457  carsggect  34477  eulerpartlemmf  34534  funpartss  36140  brresi2  37923  bnd2lem  37994  idresssidinxp  38512  disjimres  39031  aks6d1c2  42406  eqresfnbd  42510  diophrw  43022  dnnumch2  43308  lmhmlnmsplit  43350  hbtlem6  43392  dfrcl2  43936  relexpaddss  43980  cotrclrcl  44004  frege131d  44026  resimass  45505  fourierdlem42  46414  fourierdlem80  46451  isubgredgss  48132  isubgrsubgr  48136  setrecsres  49968