Theorem resss 5422

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

Syntax hints:  Vcvv 3200   ∩ cin 3573   ⊆ wss 3574   × cxp 5112   ↾ cres 5116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ss 3588  df-res 5126

This theorem is referenced by:  relssres  5437  resexg  5442  iss  5447  mptss  5454  relresfld  5662  funres  5929  funres11  5966  funcnvres  5967  2elresin  6002  fssres  6070  foimacnv  6154  frxp  7287  fnwelem  7292  tposss  7353  dftpos4  7371  smores  7449  smores2  7451  tfrlem15  7488  finresfin  8186  fidomdm  8243  imafi  8259  marypha1lem  8339  hartogslem1  8447  r0weon  8835  ackbij2lem3  9063  axdc3lem2  9273  dmct  9346  smobeth  9408  wunres  9553  vdwnnlem1  15699  symgsssg  17887  symgfisg  17888  psgnunilem5  17914  odf1o2  17988  gsumzres  18310  gsumzaddlem  18321  gsumzadd  18322  gsum2dlem2  18370  dprdfadd  18419  dprdres  18427  dprd2dlem1  18440  dprd2da  18441  opsrtoslem2  19485  lindfres  20162  txss12  21408  txbasval  21409  fmss  21750  ustneism  22027  trust  22033  isngp2  22401  equivcau  23098  cmetss  23113  volf  23297  dvcnvrelem1  23780  tdeglem4  23820  pserdv  24183  dvlog  24397  dchrelbas2  24962  issubgr2  26164  subgrprop2  26166  uhgrspansubgr  26183  hlimadd  28050  hlimcaui  28093  hhssabloilem  28118  hhsst  28123  hhsssh2  28127  hhsscms  28136  occllem  28162  nlelchi  28920  hmopidmchi  29010  fnresin  29430  imafi2  29489  omsmon  30360  carsggect  30380  eulerpartlemmf  30437  funpartss  32051  brresi  33513  bnd2lem  33590  idresssidinxp  34079  idinxpres  34088  diophrw  37322  dnnumch2  37615  lmhmlnmsplit  37657  hbtlem6  37699  dfrcl2  37966  relexpaddss  38010  cotrclrcl  38034  frege131d  38056  rnresss  39365  resimass  39449  fourierdlem42  40366  fourierdlem80  40403