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  32568  fressupp  32630  imafi2  32654  pfxrn2  32881  omsmon  34266  carsggect  34286  eulerpartlemmf  34343  funpartss  35918  brresi2  37700  bnd2lem  37771  idresssidinxp  38282  disjimres  38728  aks6d1c2  42103  eqresfnbd  42205  diophrw  42732  dnnumch2  43018  lmhmlnmsplit  43060  hbtlem6  43102  dfrcl2  43647  relexpaddss  43691  cotrclrcl  43715  frege131d  43737  resimass  45218  fourierdlem42  46130  fourierdlem80  46167  isubgredgss  47849  isubgrsubgr  47853  setrecsres  49687