Theorem resss 5619

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

Syntax hints:  Vcvv 3387   ∩ cin 3762   ⊆ wss 3763   × cxp 5303   ↾ cres 5307

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-v 3389  df-in 3770  df-ss 3777  df-res 5317

This theorem is referenced by:  relssres  5635  resexg  5641  iss  5646  mptss  5653  relresfld  5870  funres  6137  funres11  6171  funcnvres  6172  2elresin  6207  fssres  6279  foimacnv  6364  frxp  7515  fnwelem  7520  tposss  7582  dftpos4  7600  smores  7679  smores2  7681  tfrlem15  7718  finresfin  8419  fidomdm  8476  imafi  8492  marypha1lem  8572  hartogslem1  8680  r0weon  9112  ackbij2lem3  9342  axdc3lem2  9552  dmct  9625  smobeth  9687  wunres  9832  vdwnnlem1  15910  symgsssg  18082  symgfisg  18083  psgnunilem5  18109  odf1o2  18183  gsumzres  18505  gsumzaddlem  18516  gsumzadd  18517  gsum2dlem2  18565  dprdfadd  18615  dprdres  18623  dprd2dlem1  18636  dprd2da  18637  opsrtoslem2  19687  lindfres  20366  txss12  21616  txbasval  21617  fmss  21957  ustneism  22234  trust  22240  isngp2  22608  equivcau  23304  cmetss  23319  volf  23504  dvcnvrelem1  23988  tdeglem4  24028  pserdv  24391  dvlog  24605  dchrelbas2  25170  issubgr2  26374  subgrprop2  26376  uhgrspansubgr  26393  hlimadd  28372  hlimcaui  28415  hhssabloilem  28440  hhsst  28445  hhsssh2  28449  hhsscms  28458  occllem  28484  nlelchi  29242  hmopidmchi  29332  fnresin  29751  imafi2  29810  omsmon  30679  carsggect  30699  eulerpartlemmf  30756  funpartss  32366  brresi  33819  bnd2lem  33895  idresssidinxp  34389  diophrw  37818  dnnumch2  38110  lmhmlnmsplit  38152  hbtlem6  38194  dfrcl2  38460  relexpaddss  38504  cotrclrcl  38528  frege131d  38550  rnresss  39848  resimass  39927  fourierdlem42  40839  fourierdlem80  40876  setrecsres  43010