Theorem resss 5876

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

Syntax hints:  Vcvv 3408   ∩ cin 3865   ⊆ wss 3866   × cxp 5549   ↾ cres 5553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-in 3873  df-ss 3883  df-res 5563

This theorem is referenced by:  rnresss  5887  relssres  5892  resexg  5897  iss  5903  mptss  5910  relresfld  6139  funres  6422  funres11  6457  funcnvres  6458  2elresin  6498  fssres  6585  foimacnv  6678  frxp  7893  fnwelem  7898  tposss  7969  dftpos4  7987  smores  8089  smores2  8091  tfrlem15  8128  finresfin  8901  fidomdm  8953  imafiALT  8969  marypha1lem  9049  hartogslem1  9158  r0weon  9626  ackbij2lem3  9855  axdc3lem2  10065  dmct  10138  smobeth  10200  wunres  10345  vdwnnlem1  16548  symgsssg  18859  symgfisg  18860  psgnunilem5  18886  odf1o2  18962  gsumzres  19294  gsumzaddlem  19306  gsumzadd  19307  gsum2dlem2  19356  dprdfadd  19407  dprdres  19415  dprd2dlem1  19428  dprd2da  19429  lindfres  20785  opsrtoslem2  21013  txss12  22502  txbasval  22503  fmss  22843  ustneism  23121  trust  23127  isngp2  23495  equivcau  24197  metsscmetcld  24212  volf  24426  dvcnvrelem1  24914  tdeglem4OLD  24958  pserdv  25321  dvlog  25539  dchrelbas2  26118  issubgr2  27360  subgrprop2  27362  uhgrspansubgr  27379  hlimadd  29274  hlimcaui  29317  hhssabloilem  29342  hhsst  29347  hhsssh2  29351  hhsscms  29359  occllem  29384  nlelchi  30142  hmopidmchi  30232  fnresin  30680  fressupp  30742  imafi2  30766  pfxrn2  30934  omsmon  31977  carsggect  31997  eulerpartlemmf  32054  funpartss  33983  brresi2  35614  bnd2lem  35686  idresssidinxp  36181  disjimres  36595  diophrw  40284  dnnumch2  40573  lmhmlnmsplit  40615  hbtlem6  40657  dfrcl2  40959  relexpaddss  41003  cotrclrcl  41027  frege131d  41049  resimass  42456  fourierdlem42  43365  fourierdlem80  43402  setrecsres  46078