Theorem resss 6031

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

Syntax hints:  Vcvv 3488   ∩ cin 3975   ⊆ wss 3976   × cxp 5698   ↾ cres 5702

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-in 3983  df-ss 3993  df-res 5712

This theorem is referenced by:  dmresss  6040  rnresss  6046  relssres  6051  resexg  6056  iss  6064  mptss  6071  relresfld  6307  funres  6620  funres11  6655  funcnvres  6656  2elresin  6701  fssres  6787  foimacnv  6879  frxp  8167  fnwelem  8172  tposss  8268  dftpos4  8286  smores  8408  smores2  8410  tfrlem15  8448  finresfin  9332  imafi  9381  fidomdm  9402  marypha1lem  9502  hartogslem1  9611  r0weon  10081  ackbij2lem3  10309  axdc3lem2  10520  dmct  10593  smobeth  10655  wunres  10800  vdwnnlem1  17042  symgsssg  19509  symgfisg  19510  psgnunilem5  19536  odf1o2  19615  gsumzres  19951  gsumzaddlem  19963  gsumzadd  19964  gsum2dlem2  20013  dprdfadd  20064  dprdres  20072  dprd2dlem1  20085  dprd2da  20086  lindfres  21866  opsrtoslem2  22103  txss12  23634  txbasval  23635  fmss  23975  ustneism  24253  trust  24259  isngp2  24631  equivcau  25353  metsscmetcld  25368  volf  25583  dvcnvrelem1  26076  pserdv  26491  dvlog  26711  dchrelbas2  27299  issubgr2  29307  subgrprop2  29309  uhgrspansubgr  29326  hlimadd  31225  hlimcaui  31268  hhssabloilem  31293  hhsst  31298  hhsssh2  31302  hhsscms  31310  occllem  31335  nlelchi  32093  hmopidmchi  32183  fnresin  32645  fressupp  32700  imafi2  32725  pfxrn2  32906  omsmon  34263  carsggect  34283  eulerpartlemmf  34340  funpartss  35908  brresi2  37680  bnd2lem  37751  idresssidinxp  38264  disjimres  38706  aks6d1c2  42087  eqresfnbd  42227  diophrw  42715  dnnumch2  43002  lmhmlnmsplit  43044  hbtlem6  43086  dfrcl2  43636  relexpaddss  43680  cotrclrcl  43704  frege131d  43726  resimass  45148  fourierdlem42  46070  fourierdlem80  46107  isubgrsubgr  47739  setrecsres  48794