Theorem resss 5905

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

Syntax hints:  Vcvv 3422   ∩ cin 3882   ⊆ wss 3883   × cxp 5578   ↾ cres 5582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-res 5592

This theorem is referenced by:  rnresss  5916  relssres  5921  resexg  5926  iss  5932  mptss  5939  relresfld  6168  funres  6460  funres11  6495  funcnvres  6496  2elresin  6537  fssres  6624  foimacnv  6717  frxp  7938  fnwelem  7943  tposss  8014  dftpos4  8032  smores  8154  smores2  8156  tfrlem15  8194  finresfin  8974  fidomdm  9026  imafiALT  9042  marypha1lem  9122  hartogslem1  9231  r0weon  9699  ackbij2lem3  9928  axdc3lem2  10138  dmct  10211  smobeth  10273  wunres  10418  vdwnnlem1  16624  symgsssg  18990  symgfisg  18991  psgnunilem5  19017  odf1o2  19093  gsumzres  19425  gsumzaddlem  19437  gsumzadd  19438  gsum2dlem2  19487  dprdfadd  19538  dprdres  19546  dprd2dlem1  19559  dprd2da  19560  lindfres  20940  opsrtoslem2  21173  txss12  22664  txbasval  22665  fmss  23005  ustneism  23283  trust  23289  isngp2  23659  equivcau  24369  metsscmetcld  24384  volf  24598  dvcnvrelem1  25086  tdeglem4OLD  25130  pserdv  25493  dvlog  25711  dchrelbas2  26290  issubgr2  27542  subgrprop2  27544  uhgrspansubgr  27561  hlimadd  29456  hlimcaui  29499  hhssabloilem  29524  hhsst  29529  hhsssh2  29533  hhsscms  29541  occllem  29566  nlelchi  30324  hmopidmchi  30414  fnresin  30862  fressupp  30924  imafi2  30948  pfxrn2  31116  omsmon  32165  carsggect  32185  eulerpartlemmf  32242  funpartss  34173  brresi2  35804  bnd2lem  35876  idresssidinxp  36371  disjimres  36785  diophrw  40497  dnnumch2  40786  lmhmlnmsplit  40828  hbtlem6  40870  dfrcl2  41171  relexpaddss  41215  cotrclrcl  41239  frege131d  41261  resimass  42673  fourierdlem42  43580  fourierdlem80  43617  setrecsres  46293