Theorem resss 5961

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

Syntax hints:  Vcvv 3430   ∩ cin 3889   ⊆ wss 3890   × cxp 5623   ↾ cres 5627

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 3432  df-in 3897  df-ss 3907  df-res 5637

This theorem is referenced by:  dmresss  5971  rnresss  5977  relssres  5982  resexg  5987  iss  5995  mptss  6002  relresfld  6235  funres  6535  funres11  6570  funcnvres  6571  2elresin  6614  fssres  6701  foimacnv  6792  frxp  8070  fnwelem  8075  tposss  8171  dftpos4  8189  smores  8286  smores2  8288  tfrlem15  8325  finresfin  9176  imafi  9219  fidomdm  9238  imafi2  9265  marypha1lem  9340  hartogslem1  9451  r0weon  9928  ackbij2lem3  10156  axdc3lem2  10367  dmct  10440  smobeth  10503  wunres  10648  vdwnnlem1  16960  symgsssg  19436  symgfisg  19437  psgnunilem5  19463  odf1o2  19542  gsumzres  19878  gsumzaddlem  19890  gsumzadd  19891  gsum2dlem2  19940  dprdfadd  19991  dprdres  19999  dprd2dlem1  20012  dprd2da  20013  lindfres  21816  opsrtoslem2  22047  txss12  23583  txbasval  23584  fmss  23924  ustneism  24202  trust  24207  isngp2  24575  equivcau  25280  metsscmetcld  25295  volf  25509  dvcnvrelem1  25997  pserdv  26410  dvlog  26631  dchrelbas2  27217  issubgr2  29358  subgrprop2  29360  uhgrspansubgr  29377  hlimadd  31282  hlimcaui  31325  hhssabloilem  31350  hhsst  31355  hhsssh2  31359  hhsscms  31367  occllem  31392  nlelchi  32150  hmopidmchi  32240  fnresin  32715  fressupp  32779  pfxrn2  33018  omsmon  34461  carsggect  34481  eulerpartlemmf  34538  funpartss  36145  brresi2  38058  bnd2lem  38129  idresssidinxp  38652  disjimres  39188  aks6d1c2  42586  eqresfnbd  42690  diophrw  43208  dnnumch2  43494  lmhmlnmsplit  43536  hbtlem6  43578  dfrcl2  44122  relexpaddss  44166  cotrclrcl  44190  frege131d  44212  resimass  45690  fourierdlem42  46598  fourierdlem80  46635  isubgredgss  48356  isubgrsubgr  48360  setrecsres  50192