Theorem resss 5988

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

Syntax hints:  Vcvv 3455   ∩ cin 3904   ⊆ wss 3905   × cxp 5646   ↾ cres 5650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1564  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-in 3912  df-ss 3922  df-res 5660

This theorem is referenced by:  dmresss  5998  rnresss  6004  relssres  6009  resexg  6014  iss  6025  mptss  6032  cnvcnvss  6181  relresfld  6264  funres  6564  funres11  6599  funcnvres  6600  2elresin  6643  fssres  6731  foimacnv  6825  frxp  8107  fnwelem  8112  tposss  8208  dftpos4  8226  smores  8324  smores2  8326  tfrlem15  8364  finresfin  9217  imafi  9260  fidomdm  9278  imafi2  9305  marypha1lem  9380  hartogslem1  9491  r0weon  9969  ackbij2lem3  10197  axdc3lem2  10409  dmct  10482  smobeth  10545  wunres  10690  vdwnnlem1  17032  symgsssg  19508  symgfisg  19509  psgnunilem5  19535  odf1o2  19614  gsumzres  19950  gsumzaddlem  19962  gsumzadd  19963  gsum2dlem2  20012  dprdfadd  20063  dprdres  20071  dprd2dlem1  20084  dprd2da  20085  lindfres  21876  opsrtoslem2  22110  txss12  23666  txbasval  23667  fmss  24007  ustneism  24285  trust  24290  isngp2  24658  equivcau  25363  metsscmetcld  25378  volf  25592  dvcnvrelem1  26080  pserdv  26493  dvlog  26717  dchrelbas2  27302  issubgr2  29474  subgrprop2  29476  uhgrspansubgr  29493  hlimadd  31397  hlimcaui  31440  hhssabloilem  31465  hhsst  31470  hhsssh2  31474  hhsscms  31482  occllem  31507  nlelchi  32265  hmopidmchi  32355  fnresin  32827  fressupp  32891  pfxrn2  33119  omsmon  34596  carsggect  34616  eulerpartlemmf  34673  funpartss  36295  brresi2  38220  bnd2lem  38291  idresssidinxp  38814  disjimres  39350  aks6d1c2  42748  eqresfnbd  42852  diophrw  43341  dnnumch2  43623  lmhmlnmsplit  43665  hbtlem6  43707  dfrcl2  44251  relexpaddss  44295  cotrclrcl  44319  frege131d  44341  resimass  45816  fourierdlem42  46724  fourierdlem80  46761  isubgredgss  48488  isubgrsubgr  48492  setrecsres  50324