Theorem resss 6018

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

Syntax hints:  Vcvv 3479   ∩ cin 3949   ⊆ wss 3950   × cxp 5682   ↾ cres 5686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-in 3957  df-ss 3967  df-res 5696

This theorem is referenced by:  dmresss  6028  rnresss  6034  relssres  6039  resexg  6044  iss  6052  mptss  6059  relresfld  6295  funres  6607  funres11  6642  funcnvres  6643  2elresin  6688  fssres  6773  foimacnv  6864  frxp  8152  fnwelem  8157  tposss  8253  dftpos4  8271  smores  8393  smores2  8395  tfrlem15  8433  finresfin  9305  imafi  9354  fidomdm  9375  marypha1lem  9474  hartogslem1  9583  r0weon  10053  ackbij2lem3  10281  axdc3lem2  10492  dmct  10565  smobeth  10627  wunres  10772  vdwnnlem1  17034  symgsssg  19486  symgfisg  19487  psgnunilem5  19513  odf1o2  19592  gsumzres  19928  gsumzaddlem  19940  gsumzadd  19941  gsum2dlem2  19990  dprdfadd  20041  dprdres  20049  dprd2dlem1  20062  dprd2da  20063  lindfres  21844  opsrtoslem2  22081  txss12  23614  txbasval  23615  fmss  23955  ustneism  24233  trust  24239  isngp2  24611  equivcau  25335  metsscmetcld  25350  volf  25565  dvcnvrelem1  26057  pserdv  26474  dvlog  26694  dchrelbas2  27282  issubgr2  29290  subgrprop2  29292  uhgrspansubgr  29309  hlimadd  31213  hlimcaui  31256  hhssabloilem  31281  hhsst  31286  hhsssh2  31290  hhsscms  31298  occllem  31323  nlelchi  32081  hmopidmchi  32171  fnresin  32637  fressupp  32698  imafi2  32724  pfxrn2  32925  omsmon  34301  carsggect  34321  eulerpartlemmf  34378  funpartss  35946  brresi2  37728  bnd2lem  37799  idresssidinxp  38310  disjimres  38752  aks6d1c2  42132  eqresfnbd  42273  diophrw  42775  dnnumch2  43062  lmhmlnmsplit  43104  hbtlem6  43146  dfrcl2  43692  relexpaddss  43736  cotrclrcl  43760  frege131d  43782  resimass  45251  fourierdlem42  46169  fourierdlem80  46206  isubgredgss  47856  isubgrsubgr  47860  setrecsres  49276