Theorem resss 6007

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

Syntax hints:  Vcvv 3475   ∩ cin 3948   ⊆ wss 3949   × cxp 5675   ↾ cres 5679

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-res 5689

This theorem is referenced by:  rnresss  6018  relssres  6023  resexg  6028  iss  6036  mptss  6043  relresfld  6276  funres  6591  funres11  6626  funcnvres  6627  2elresin  6672  fssres  6758  foimacnv  6851  frxp  8112  fnwelem  8117  tposss  8212  dftpos4  8230  smores  8352  smores2  8354  tfrlem15  8392  finresfin  9270  fidomdm  9329  imafiALT  9345  marypha1lem  9428  hartogslem1  9537  r0weon  10007  ackbij2lem3  10236  axdc3lem2  10446  dmct  10519  smobeth  10581  wunres  10726  vdwnnlem1  16928  symgsssg  19335  symgfisg  19336  psgnunilem5  19362  odf1o2  19441  gsumzres  19777  gsumzaddlem  19789  gsumzadd  19790  gsum2dlem2  19839  dprdfadd  19890  dprdres  19898  dprd2dlem1  19911  dprd2da  19912  lindfres  21378  opsrtoslem2  21617  txss12  23109  txbasval  23110  fmss  23450  ustneism  23728  trust  23734  isngp2  24106  equivcau  24817  metsscmetcld  24832  volf  25046  dvcnvrelem1  25534  tdeglem4OLD  25578  pserdv  25941  dvlog  26159  dchrelbas2  26740  issubgr2  28529  subgrprop2  28531  uhgrspansubgr  28548  hlimadd  30446  hlimcaui  30489  hhssabloilem  30514  hhsst  30519  hhsssh2  30523  hhsscms  30531  occllem  30556  nlelchi  31314  hmopidmchi  31404  fnresin  31850  fressupp  31910  imafi2  31936  pfxrn2  32106  omsmon  33297  carsggect  33317  eulerpartlemmf  33374  funpartss  34916  brresi2  36588  bnd2lem  36659  idresssidinxp  37177  disjimres  37620  eqresfnbd  41054  diophrw  41497  dnnumch2  41787  lmhmlnmsplit  41829  hbtlem6  41871  dfrcl2  42425  relexpaddss  42469  cotrclrcl  42493  frege131d  42515  resimass  43943  fourierdlem42  44865  fourierdlem80  44902  setrecsres  47747