Theorem resss 5997

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

This proof depends on syntax axioms:  Vcvv 3454   ⊆ wss 3900   ∩ cin 4092   × cxp 5653   ↾ cres 5657

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-in 4094  df-res 5667

This theorem is used by:  dmresss  6008  rnresss  6012  relssres  6017  resexg  6022  iss  6033  mptss  6040  cnvcnvss  6192  relresfldOLD  6286  funres  6591  funres11  6628  funcnvres  6629  2elresin  6671  fssres  6759  foimacnv  6853  frxp  8151  fnwelem  8156  tposss  8258  dftpos4  8276  smores2  8376  tfrlem15  8414  finresfin  9277  imafi  9321  fidomdm  9337  imafi2  9364  marypha1lem  9438  hartogslem1  9549  r0weon  10104  ackbij2lem3  10331  axdc3lem2  10542  dmct  10615  dmctOLD  10616  smobeth  10684  wunres  10829  vdwnnlem1  17188  symgsssg  19696  symgfisg  19697  psgnunilem5  19723  odf1o2  19802  gsumzres  20138  gsumzaddlem  20150  gsumzadd  20151  gsum2dlem2  20200  dprdfadd  20251  dprdres  20259  dprd2dlem1  20272  dprd2da  20273  lindfres  22144  opsrtoslem2  22380  txss12  23939  txbasval  23940  fmss  24280  ustneism  24558  trust  24563  isngp2  24931  equivcau  25636  metsscmetcld  25651  volf  25865  dvcnvrelem1  26352  pserdv  26771  dvlog  26994  dchrelbas2  27579  issubgr2  29868  subgrprop2  29870  uhgrspansubgr  29887  hlimadd  31810  hlimcaui  31853  hhssabloilem  31878  hhsst  31883  hhsssh2  31887  hhsscms  31895  occllem  31920  nlelchi  32678  hmopidmchi  32768  fnresin  33275  fressupp  33338  pfxrn2  33563  omsmon  34986  carsggect  35006  eulerpartlemmf  35063  funpartss  36838  relssresv  38096  brresi2  38797  bnd2lem  38868  idresssidinxp  39389  disjimres  39925  aks6d1c2  43323  eqresfnbd  43429  diophrw  43913  dnnumch2  44195  lmhmlnmsplit  44232  hbtlem6  44274  dfrcl2  44817  relexpaddss  44861  cotrclrcl  44885  frege131d  44907  resimass  46394  fourierdlem42  47301  fourierdlem80  47338  isubgredgss  49105  isubgrsubgr  49109  setrecsres  51012