Theorem resss 6000

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

Syntax hints:  Vcvv 3455   ∩ cin 3904   ⊆ wss 3905   × cxp 5659   ↾ cres 5663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-in 3912  df-ss 3922  df-res 5673

This theorem is referenced by:  dmresss  6010  rnresss  6016  relssres  6021  resexg  6026  iss  6037  mptss  6044  cnvcnvss  6192  relresfld  6277  funres  6578  funres11  6613  funcnvres  6614  2elresin  6656  fssres  6744  foimacnv  6838  frxp  8118  fnwelem  8123  tposss  8219  dftpos4  8237  smores  8335  smores2  8337  tfrlem15  8375  finresfin  9228  imafi  9271  fidomdm  9287  imafi2  9314  marypha1lem  9389  hartogslem1  9500  r0weon  9992  ackbij2lem3  10219  axdc3lem2  10430  dmct  10503  smobeth  10566  wunres  10711  vdwnnlem1  17050  symgsssg  19532  symgfisg  19533  psgnunilem5  19559  odf1o2  19638  gsumzres  19974  gsumzaddlem  19986  gsumzadd  19987  gsum2dlem2  20036  dprdfadd  20087  dprdres  20095  dprd2dlem1  20108  dprd2da  20109  lindfres  21973  opsrtoslem2  22207  txss12  23762  txbasval  23763  fmss  24103  ustneism  24381  trust  24386  isngp2  24754  equivcau  25459  metsscmetcld  25474  volf  25688  dvcnvrelem1  26176  pserdv  26592  dvlog  26816  dchrelbas2  27401  issubgr2  29622  subgrprop2  29624  uhgrspansubgr  29641  hlimadd  31545  hlimcaui  31588  hhssabloilem  31613  hhsst  31618  hhsssh2  31622  hhsscms  31630  occllem  31655  nlelchi  32413  hmopidmchi  32503  fnresin  32969  fressupp  33033  pfxrn2  33260  omsmon  34688  carsggect  34708  eulerpartlemmf  34765  funpartss  36436  brresi2  38391  bnd2lem  38462  idresssidinxp  38983  disjimres  39519  aks6d1c2  42917  eqresfnbd  43023  diophrw  43510  dnnumch2  43792  lmhmlnmsplit  43834  hbtlem6  43876  dfrcl2  44420  relexpaddss  44464  cotrclrcl  44488  frege131d  44510  resimass  45975  fourierdlem42  46883  fourierdlem80  46920  isubgredgss  48650  isubgrsubgr  48654  setrecsres  50500