Theorem resss 5966

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

Syntax hints:  Vcvv 3429   ∩ cin 3888   ⊆ wss 3889   × cxp 5629   ↾ cres 5633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-in 3896  df-ss 3906  df-res 5643

This theorem is referenced by:  dmresss  5976  rnresss  5982  relssres  5987  resexg  5992  iss  6000  mptss  6007  relresfld  6240  funres  6540  funres11  6575  funcnvres  6576  2elresin  6619  fssres  6706  foimacnv  6797  frxp  8076  fnwelem  8081  tposss  8177  dftpos4  8195  smores  8292  smores2  8294  tfrlem15  8331  finresfin  9182  imafi  9225  fidomdm  9244  imafi2  9271  marypha1lem  9346  hartogslem1  9457  r0weon  9934  ackbij2lem3  10162  axdc3lem2  10373  dmct  10446  smobeth  10509  wunres  10654  vdwnnlem1  16966  symgsssg  19442  symgfisg  19443  psgnunilem5  19469  odf1o2  19548  gsumzres  19884  gsumzaddlem  19896  gsumzadd  19897  gsum2dlem2  19946  dprdfadd  19997  dprdres  20005  dprd2dlem1  20018  dprd2da  20019  lindfres  21803  opsrtoslem2  22034  txss12  23570  txbasval  23571  fmss  23911  ustneism  24189  trust  24194  isngp2  24562  equivcau  25267  metsscmetcld  25282  volf  25496  dvcnvrelem1  25984  pserdv  26394  dvlog  26615  dchrelbas2  27200  issubgr2  29341  subgrprop2  29343  uhgrspansubgr  29360  hlimadd  31264  hlimcaui  31307  hhssabloilem  31332  hhsst  31337  hhsssh2  31341  hhsscms  31349  occllem  31374  nlelchi  32132  hmopidmchi  32222  fnresin  32697  fressupp  32761  pfxrn2  33000  omsmon  34442  carsggect  34462  eulerpartlemmf  34519  funpartss  36126  brresi2  38041  bnd2lem  38112  idresssidinxp  38635  disjimres  39171  aks6d1c2  42569  eqresfnbd  42673  diophrw  43191  dnnumch2  43473  lmhmlnmsplit  43515  hbtlem6  43557  dfrcl2  44101  relexpaddss  44145  cotrclrcl  44169  frege131d  44191  resimass  45669  fourierdlem42  46577  fourierdlem80  46614  isubgredgss  48341  isubgrsubgr  48345  setrecsres  50177