Theorem resss 5916

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

Syntax hints:  Vcvv 3432   ∩ cin 3886   ⊆ wss 3887   × cxp 5587   ↾ cres 5591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-res 5601

This theorem is referenced by:  rnresss  5927  relssres  5932  resexg  5937  iss  5943  mptss  5950  relresfld  6179  funres  6476  funres11  6511  funcnvres  6512  2elresin  6553  fssres  6640  foimacnv  6733  frxp  7967  fnwelem  7972  tposss  8043  dftpos4  8061  smores  8183  smores2  8185  tfrlem15  8223  finresfin  9045  fidomdm  9096  imafiALT  9112  marypha1lem  9192  hartogslem1  9301  r0weon  9768  ackbij2lem3  9997  axdc3lem2  10207  dmct  10280  smobeth  10342  wunres  10487  vdwnnlem1  16696  symgsssg  19075  symgfisg  19076  psgnunilem5  19102  odf1o2  19178  gsumzres  19510  gsumzaddlem  19522  gsumzadd  19523  gsum2dlem2  19572  dprdfadd  19623  dprdres  19631  dprd2dlem1  19644  dprd2da  19645  lindfres  21030  opsrtoslem2  21263  txss12  22756  txbasval  22757  fmss  23097  ustneism  23375  trust  23381  isngp2  23753  equivcau  24464  metsscmetcld  24479  volf  24693  dvcnvrelem1  25181  tdeglem4OLD  25225  pserdv  25588  dvlog  25806  dchrelbas2  26385  issubgr2  27639  subgrprop2  27641  uhgrspansubgr  27658  hlimadd  29555  hlimcaui  29598  hhssabloilem  29623  hhsst  29628  hhsssh2  29632  hhsscms  29640  occllem  29665  nlelchi  30423  hmopidmchi  30513  fnresin  30961  fressupp  31022  imafi2  31046  pfxrn2  31214  omsmon  32265  carsggect  32285  eulerpartlemmf  32342  funpartss  34246  brresi2  35877  bnd2lem  35949  idresssidinxp  36444  disjimres  36858  diophrw  40581  dnnumch2  40870  lmhmlnmsplit  40912  hbtlem6  40954  dfrcl2  41282  relexpaddss  41326  cotrclrcl  41350  frege131d  41372  resimass  42784  fourierdlem42  43690  fourierdlem80  43727  setrecsres  46407