Theorem resss 6022

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

Syntax hints:  Vcvv 3478   ∩ cin 3962   ⊆ wss 3963   × cxp 5687   ↾ cres 5691

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-in 3970  df-ss 3980  df-res 5701

This theorem is referenced by:  dmresss  6031  rnresss  6037  relssres  6042  resexg  6047  iss  6055  mptss  6062  relresfld  6298  funres  6610  funres11  6645  funcnvres  6646  2elresin  6690  fssres  6775  foimacnv  6866  frxp  8150  fnwelem  8155  tposss  8251  dftpos4  8269  smores  8391  smores2  8393  tfrlem15  8431  finresfin  9302  imafi  9351  fidomdm  9372  marypha1lem  9471  hartogslem1  9580  r0weon  10050  ackbij2lem3  10278  axdc3lem2  10489  dmct  10562  smobeth  10624  wunres  10769  vdwnnlem1  17029  symgsssg  19500  symgfisg  19501  psgnunilem5  19527  odf1o2  19606  gsumzres  19942  gsumzaddlem  19954  gsumzadd  19955  gsum2dlem2  20004  dprdfadd  20055  dprdres  20063  dprd2dlem1  20076  dprd2da  20077  lindfres  21861  opsrtoslem2  22098  txss12  23629  txbasval  23630  fmss  23970  ustneism  24248  trust  24254  isngp2  24626  equivcau  25348  metsscmetcld  25363  volf  25578  dvcnvrelem1  26071  pserdv  26488  dvlog  26708  dchrelbas2  27296  issubgr2  29304  subgrprop2  29306  uhgrspansubgr  29323  hlimadd  31222  hlimcaui  31265  hhssabloilem  31290  hhsst  31295  hhsssh2  31299  hhsscms  31307  occllem  31332  nlelchi  32090  hmopidmchi  32180  fnresin  32643  fressupp  32703  imafi2  32729  pfxrn2  32909  omsmon  34280  carsggect  34300  eulerpartlemmf  34357  funpartss  35926  brresi2  37707  bnd2lem  37778  idresssidinxp  38290  disjimres  38732  aks6d1c2  42112  eqresfnbd  42252  diophrw  42747  dnnumch2  43034  lmhmlnmsplit  43076  hbtlem6  43118  dfrcl2  43664  relexpaddss  43708  cotrclrcl  43732  frege131d  43754  resimass  45184  fourierdlem42  46105  fourierdlem80  46142  isubgredgss  47789  isubgrsubgr  47793  setrecsres  48933