Theorem resss 5972

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

Syntax hints:  Vcvv 3447   ∩ cin 3913   ⊆ wss 3914   × cxp 5636   ↾ cres 5640

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 3449  df-in 3921  df-ss 3931  df-res 5650

This theorem is referenced by:  dmresss  5982  rnresss  5988  relssres  5993  resexg  5998  iss  6006  mptss  6013  relresfld  6249  funres  6558  funres11  6593  funcnvres  6594  2elresin  6639  fssres  6726  foimacnv  6817  frxp  8105  fnwelem  8110  tposss  8206  dftpos4  8224  smores  8321  smores2  8323  tfrlem15  8360  finresfin  9215  imafi  9264  fidomdm  9285  marypha1lem  9384  hartogslem1  9495  r0weon  9965  ackbij2lem3  10193  axdc3lem2  10404  dmct  10477  smobeth  10539  wunres  10684  vdwnnlem1  16966  symgsssg  19397  symgfisg  19398  psgnunilem5  19424  odf1o2  19503  gsumzres  19839  gsumzaddlem  19851  gsumzadd  19852  gsum2dlem2  19901  dprdfadd  19952  dprdres  19960  dprd2dlem1  19973  dprd2da  19974  lindfres  21732  opsrtoslem2  21963  txss12  23492  txbasval  23493  fmss  23833  ustneism  24111  trust  24117  isngp2  24485  equivcau  25200  metsscmetcld  25215  volf  25430  dvcnvrelem1  25922  pserdv  26339  dvlog  26560  dchrelbas2  27148  issubgr2  29199  subgrprop2  29201  uhgrspansubgr  29218  hlimadd  31122  hlimcaui  31165  hhssabloilem  31190  hhsst  31195  hhsssh2  31199  hhsscms  31207  occllem  31232  nlelchi  31990  hmopidmchi  32080  fnresin  32550  fressupp  32611  imafi2  32635  pfxrn2  32861  omsmon  34289  carsggect  34309  eulerpartlemmf  34366  funpartss  35932  brresi2  37714  bnd2lem  37785  idresssidinxp  38296  disjimres  38742  aks6d1c2  42118  eqresfnbd  42220  diophrw  42747  dnnumch2  43034  lmhmlnmsplit  43076  hbtlem6  43118  dfrcl2  43663  relexpaddss  43707  cotrclrcl  43731  frege131d  43753  resimass  45234  fourierdlem42  46147  fourierdlem80  46184  isubgredgss  47865  isubgrsubgr  47869  setrecsres  49691