Theorem resss 5993

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

Syntax hints:  Vcvv 3464   ∩ cin 3930   ⊆ wss 3931   × cxp 5657   ↾ cres 5661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-in 3938  df-ss 3948  df-res 5671

This theorem is referenced by:  dmresss  6003  rnresss  6009  relssres  6014  resexg  6019  iss  6027  mptss  6034  relresfld  6270  funres  6583  funres11  6618  funcnvres  6619  2elresin  6664  fssres  6749  foimacnv  6840  frxp  8130  fnwelem  8135  tposss  8231  dftpos4  8249  smores  8371  smores2  8373  tfrlem15  8411  finresfin  9281  imafi  9330  fidomdm  9351  marypha1lem  9450  hartogslem1  9561  r0weon  10031  ackbij2lem3  10259  axdc3lem2  10470  dmct  10543  smobeth  10605  wunres  10750  vdwnnlem1  17020  symgsssg  19453  symgfisg  19454  psgnunilem5  19480  odf1o2  19559  gsumzres  19895  gsumzaddlem  19907  gsumzadd  19908  gsum2dlem2  19957  dprdfadd  20008  dprdres  20016  dprd2dlem1  20029  dprd2da  20030  lindfres  21788  opsrtoslem2  22019  txss12  23548  txbasval  23549  fmss  23889  ustneism  24167  trust  24173  isngp2  24541  equivcau  25257  metsscmetcld  25272  volf  25487  dvcnvrelem1  25979  pserdv  26396  dvlog  26617  dchrelbas2  27205  issubgr2  29256  subgrprop2  29258  uhgrspansubgr  29275  hlimadd  31179  hlimcaui  31222  hhssabloilem  31247  hhsst  31252  hhsssh2  31256  hhsscms  31264  occllem  31289  nlelchi  32047  hmopidmchi  32137  fnresin  32609  fressupp  32670  imafi2  32694  pfxrn2  32920  omsmon  34335  carsggect  34355  eulerpartlemmf  34412  funpartss  35967  brresi2  37749  bnd2lem  37820  idresssidinxp  38331  disjimres  38773  aks6d1c2  42148  eqresfnbd  42250  diophrw  42757  dnnumch2  43044  lmhmlnmsplit  43086  hbtlem6  43128  dfrcl2  43673  relexpaddss  43717  cotrclrcl  43741  frege131d  43763  resimass  45244  fourierdlem42  46158  fourierdlem80  46195  isubgredgss  47858  isubgrsubgr  47862  setrecsres  49546