Theorem resss 5952

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

Syntax hints:  Vcvv 3436   ∩ cin 3902   ⊆ wss 3903   × cxp 5617   ↾ cres 5621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-in 3910  df-ss 3920  df-res 5631

This theorem is referenced by:  dmresss  5962  rnresss  5968  relssres  5973  resexg  5978  iss  5986  mptss  5993  relresfld  6224  funres  6524  funres11  6559  funcnvres  6560  2elresin  6603  fssres  6690  foimacnv  6781  frxp  8059  fnwelem  8064  tposss  8160  dftpos4  8178  smores  8275  smores2  8277  tfrlem15  8314  finresfin  9161  imafi  9204  fidomdm  9224  marypha1lem  9323  hartogslem1  9434  r0weon  9906  ackbij2lem3  10134  axdc3lem2  10345  dmct  10418  smobeth  10480  wunres  10625  vdwnnlem1  16907  symgsssg  19346  symgfisg  19347  psgnunilem5  19373  odf1o2  19452  gsumzres  19788  gsumzaddlem  19800  gsumzadd  19801  gsum2dlem2  19850  dprdfadd  19901  dprdres  19909  dprd2dlem1  19922  dprd2da  19923  lindfres  21730  opsrtoslem2  21961  txss12  23490  txbasval  23491  fmss  23831  ustneism  24109  trust  24115  isngp2  24483  equivcau  25198  metsscmetcld  25213  volf  25428  dvcnvrelem1  25920  pserdv  26337  dvlog  26558  dchrelbas2  27146  issubgr2  29217  subgrprop2  29219  uhgrspansubgr  29236  hlimadd  31137  hlimcaui  31180  hhssabloilem  31205  hhsst  31210  hhsssh2  31214  hhsscms  31222  occllem  31247  nlelchi  32005  hmopidmchi  32095  fnresin  32569  fressupp  32631  imafi2  32655  pfxrn2  32882  omsmon  34272  carsggect  34292  eulerpartlemmf  34349  funpartss  35928  brresi2  37710  bnd2lem  37781  idresssidinxp  38292  disjimres  38738  aks6d1c2  42113  eqresfnbd  42215  diophrw  42742  dnnumch2  43028  lmhmlnmsplit  43070  hbtlem6  43112  dfrcl2  43657  relexpaddss  43701  cotrclrcl  43725  frege131d  43747  resimass  45228  fourierdlem42  46140  fourierdlem80  46177  isubgredgss  47859  isubgrsubgr  47863  setrecsres  49697