Theorem resss 5968

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

Syntax hints:  Vcvv 3442   ∩ cin 3902   ⊆ wss 3903   × cxp 5630   ↾ cres 5634

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-in 3910  df-ss 3920  df-res 5644

This theorem is referenced by:  dmresss  5978  rnresss  5984  relssres  5989  resexg  5994  iss  6002  mptss  6009  relresfld  6242  funres  6542  funres11  6577  funcnvres  6578  2elresin  6621  fssres  6708  foimacnv  6799  frxp  8078  fnwelem  8083  tposss  8179  dftpos4  8197  smores  8294  smores2  8296  tfrlem15  8333  finresfin  9184  imafi  9227  fidomdm  9246  imafi2  9273  marypha1lem  9348  hartogslem1  9459  r0weon  9934  ackbij2lem3  10162  axdc3lem2  10373  dmct  10446  smobeth  10509  wunres  10654  vdwnnlem1  16935  symgsssg  19411  symgfisg  19412  psgnunilem5  19438  odf1o2  19517  gsumzres  19853  gsumzaddlem  19865  gsumzadd  19866  gsum2dlem2  19915  dprdfadd  19966  dprdres  19974  dprd2dlem1  19987  dprd2da  19988  lindfres  21793  opsrtoslem2  22026  txss12  23564  txbasval  23565  fmss  23905  ustneism  24183  trust  24188  isngp2  24556  equivcau  25271  metsscmetcld  25286  volf  25501  dvcnvrelem1  25993  pserdv  26410  dvlog  26631  dchrelbas2  27219  issubgr2  29361  subgrprop2  29363  uhgrspansubgr  29380  hlimadd  31285  hlimcaui  31328  hhssabloilem  31353  hhsst  31358  hhsssh2  31362  hhsscms  31370  occllem  31395  nlelchi  32153  hmopidmchi  32243  fnresin  32718  fressupp  32782  pfxrn2  33037  omsmon  34480  carsggect  34500  eulerpartlemmf  34557  funpartss  36164  brresi2  37975  bnd2lem  38046  idresssidinxp  38569  disjimres  39105  aks6d1c2  42504  eqresfnbd  42608  diophrw  43120  dnnumch2  43406  lmhmlnmsplit  43448  hbtlem6  43490  dfrcl2  44034  relexpaddss  44078  cotrclrcl  44102  frege131d  44124  resimass  45602  fourierdlem42  46511  fourierdlem80  46548  isubgredgss  48229  isubgrsubgr  48233  setrecsres  50065