Theorem resss 5872

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

Syntax hints:  Vcvv 3494   ∩ cin 3934   ⊆ wss 3935   × cxp 5547   ↾ cres 5551

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3942  df-ss 3951  df-res 5561

This theorem is referenced by:  relssres  5887  resexg  5892  iss  5897  mptss  5904  relresfld  6121  funres  6391  funres11  6425  funcnvres  6426  2elresin  6462  fssres  6538  foimacnv  6626  frxp  7814  fnwelem  7819  tposss  7887  dftpos4  7905  smores  7983  smores2  7985  tfrlem15  8022  finresfin  8738  fidomdm  8795  imafi  8811  marypha1lem  8891  hartogslem1  9000  r0weon  9432  ackbij2lem3  9657  axdc3lem2  9867  dmct  9940  smobeth  10002  wunres  10147  vdwnnlem1  16325  symgsssg  18589  symgfisg  18590  psgnunilem5  18616  odf1o2  18692  gsumzres  19023  gsumzaddlem  19035  gsumzadd  19036  gsum2dlem2  19085  dprdfadd  19136  dprdres  19144  dprd2dlem1  19157  dprd2da  19158  opsrtoslem2  20259  lindfres  20961  txss12  22207  txbasval  22208  fmss  22548  ustneism  22826  trust  22832  isngp2  23200  equivcau  23897  metsscmetcld  23912  volf  24124  dvcnvrelem1  24608  tdeglem4  24648  pserdv  25011  dvlog  25228  dchrelbas2  25807  issubgr2  27048  subgrprop2  27050  uhgrspansubgr  27067  hlimadd  28964  hlimcaui  29007  hhssabloilem  29032  hhsst  29037  hhsssh2  29041  hhsscms  29049  occllem  29074  nlelchi  29832  hmopidmchi  29922  fnresin  30365  imafi2  30441  pfxrn2  30611  omsmon  31551  carsggect  31571  eulerpartlemmf  31628  funpartss  33400  brresi2  34988  bnd2lem  35063  idresssidinxp  35560  disjimres  35974  diophrw  39349  dnnumch2  39638  lmhmlnmsplit  39680  hbtlem6  39722  dfrcl2  40012  relexpaddss  40056  cotrclrcl  40080  frege131d  40102  rnresss  41432  resimass  41503  fourierdlem42  42428  fourierdlem80  42465  setrecsres  44798