Theorem resss 5954

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

Syntax hints:  Vcvv 3431   ∩ cin 3882   ⊆ wss 3883   × cxp 5617   ↾ cres 5621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-in 3890  df-ss 3900  df-res 5631

This theorem is referenced by:  dmresss  5964  rnresss  5970  relssres  5975  resexg  5980  iss  5988  mptss  5995  relresfld  6228  funres  6528  funres11  6563  funcnvres  6564  2elresin  6607  fssres  6694  foimacnv  6785  frxp  8067  fnwelem  8072  tposss  8168  dftpos4  8186  smores  8283  smores2  8285  tfrlem15  8322  finresfin  9173  imafi  9216  fidomdm  9235  imafi2  9262  marypha1lem  9337  hartogslem1  9448  r0weon  9926  ackbij2lem3  10154  axdc3lem2  10365  dmct  10438  smobeth  10501  wunres  10646  vdwnnlem1  16958  symgsssg  19434  symgfisg  19435  psgnunilem5  19461  odf1o2  19540  gsumzres  19876  gsumzaddlem  19888  gsumzadd  19889  gsum2dlem2  19938  dprdfadd  19989  dprdres  19997  dprd2dlem1  20010  dprd2da  20011  lindfres  21799  opsrtoslem2  22033  txss12  23589  txbasval  23590  fmss  23930  ustneism  24208  trust  24213  isngp2  24581  equivcau  25286  metsscmetcld  25301  volf  25515  dvcnvrelem1  26003  pserdv  26413  dvlog  26634  dchrelbas2  27219  issubgr2  29360  subgrprop2  29362  uhgrspansubgr  29379  hlimadd  31283  hlimcaui  31326  hhssabloilem  31351  hhsst  31356  hhsssh2  31360  hhsscms  31368  occllem  31393  nlelchi  32151  hmopidmchi  32241  fnresin  32717  fressupp  32781  pfxrn2  33020  omsmon  34491  carsggect  34511  eulerpartlemmf  34568  funpartss  36181  brresi2  38096  bnd2lem  38167  idresssidinxp  38690  disjimres  39226  aks6d1c2  42624  eqresfnbd  42728  diophrw  43217  dnnumch2  43499  lmhmlnmsplit  43541  hbtlem6  43583  dfrcl2  44127  relexpaddss  44171  cotrclrcl  44195  frege131d  44217  resimass  45692  fourierdlem42  46600  fourierdlem80  46637  isubgredgss  48364  isubgrsubgr  48368  setrecsres  50200