Theorem resss 6002

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

This proof depends on syntax axioms:  Vcvv 3457   ∩ cin 3905   ⊆ wss 3906   × cxp 5661   ↾ cres 5665

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3913  df-ss 3923  df-res 5675

This theorem is used by:  dmresss  6012  rnresss  6018  relssres  6023  resexg  6028  iss  6039  mptss  6046  cnvcnvss  6194  relresfldOLD  6281  funres  6582  funres11  6617  funcnvres  6618  2elresin  6660  fssres  6748  foimacnv  6842  frxp  8128  fnwelem  8133  tposss  8229  dftpos4  8247  smores  8345  smores2  8347  tfrlem15  8385  finresfin  9239  imafi  9282  fidomdm  9298  imafi2  9325  marypha1lem  9400  hartogslem1  9511  r0weon  10012  ackbij2lem3  10239  axdc3lem2  10450  dmct  10523  smobeth  10588  wunres  10733  vdwnnlem1  17079  symgsssg  19583  symgfisg  19584  psgnunilem5  19610  odf1o2  19689  gsumzres  20025  gsumzaddlem  20037  gsumzadd  20038  gsum2dlem2  20087  dprdfadd  20138  dprdres  20146  dprd2dlem1  20159  dprd2da  20160  lindfres  22025  opsrtoslem2  22259  txss12  23815  txbasval  23816  fmss  24156  ustneism  24434  trust  24439  isngp2  24807  equivcau  25512  metsscmetcld  25527  volf  25741  dvcnvrelem1  26229  pserdv  26645  dvlog  26869  dchrelbas2  27454  issubgr2  29682  subgrprop2  29684  uhgrspansubgr  29701  hlimadd  31618  hlimcaui  31661  hhssabloilem  31686  hhsst  31691  hhsssh2  31695  hhsscms  31703  occllem  31728  nlelchi  32486  hmopidmchi  32576  fnresin  33042  fressupp  33106  pfxrn2  33332  omsmon  34755  carsggect  34775  eulerpartlemmf  34832  funpartss  36475  brresi2  38431  bnd2lem  38502  idresssidinxp  39023  disjimres  39559  aks6d1c2  42957  eqresfnbd  43063  diophrw  43550  dnnumch2  43832  lmhmlnmsplit  43874  hbtlem6  43916  dfrcl2  44460  relexpaddss  44504  cotrclrcl  44528  frege131d  44550  resimass  46015  fourierdlem42  46923  fourierdlem80  46960  isubgredgss  48690  isubgrsubgr  48694  setrecsres  50539