Theorem resss 6011

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

Syntax hints:  Vcvv 3462   ∩ cin 3946   ⊆ wss 3947   × cxp 5680   ↾ cres 5684

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-in 3954  df-ss 3964  df-res 5694

This theorem is referenced by:  dmresss  6020  rnresss  6026  relssres  6031  resexg  6036  iss  6044  mptss  6051  relresfld  6287  funres  6601  funres11  6636  funcnvres  6637  2elresin  6682  fssres  6768  foimacnv  6860  frxp  8140  fnwelem  8145  tposss  8242  dftpos4  8260  smores  8382  smores2  8384  tfrlem15  8422  finresfin  9304  imafi  9355  fidomdm  9376  marypha1lem  9476  hartogslem1  9585  r0weon  10055  ackbij2lem3  10284  axdc3lem2  10494  dmct  10567  smobeth  10629  wunres  10774  vdwnnlem1  16997  symgsssg  19465  symgfisg  19466  psgnunilem5  19492  odf1o2  19571  gsumzres  19907  gsumzaddlem  19919  gsumzadd  19920  gsum2dlem2  19969  dprdfadd  20020  dprdres  20028  dprd2dlem1  20041  dprd2da  20042  lindfres  21821  opsrtoslem2  22069  txss12  23600  txbasval  23601  fmss  23941  ustneism  24219  trust  24225  isngp2  24597  equivcau  25319  metsscmetcld  25334  volf  25549  dvcnvrelem1  26041  tdeglem4OLD  26087  pserdv  26459  dvlog  26678  dchrelbas2  27266  issubgr2  29208  subgrprop2  29210  uhgrspansubgr  29227  hlimadd  31126  hlimcaui  31169  hhssabloilem  31194  hhsst  31199  hhsssh2  31203  hhsscms  31211  occllem  31236  nlelchi  31994  hmopidmchi  32084  fnresin  32543  fressupp  32600  imafi2  32625  pfxrn2  32803  omsmon  34132  carsggect  34152  eulerpartlemmf  34209  funpartss  35768  brresi2  37421  bnd2lem  37492  idresssidinxp  38006  disjimres  38448  aks6d1c2  41828  eqresfnbd  41956  diophrw  42416  dnnumch2  42706  lmhmlnmsplit  42748  hbtlem6  42790  dfrcl2  43341  relexpaddss  43385  cotrclrcl  43409  frege131d  43431  resimass  44848  fourierdlem42  45770  fourierdlem80  45807  isubgrsubgr  47434  setrecsres  48448