Theorem resss 5992

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

This proof depends on syntax axioms:  Vcvv 3451   ∩ cin 3898   ⊆ wss 3899   × cxp 5649   ↾ cres 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-in 3906  df-ss 3916  df-res 5663

This theorem is used by:  dmresss  6002  rnresss  6006  relssres  6011  resexg  6016  iss  6027  mptss  6034  cnvcnvss  6186  relresfldOLD  6279  funres  6582  funres11  6617  funcnvres  6618  2elresin  6660  fssres  6748  foimacnv  6842  frxp  8138  fnwelem  8143  tposss  8244  dftpos4  8262  smores  8360  smores2  8362  tfrlem15  8400  finresfin  9263  imafi  9307  fidomdm  9323  imafi2  9350  marypha1lem  9425  hartogslem1  9536  r0weon  10091  ackbij2lem3  10318  axdc3lem2  10529  dmct  10602  dmctOLD  10603  smobeth  10671  wunres  10816  vdwnnlem1  17173  symgsssg  19681  symgfisg  19682  psgnunilem5  19708  odf1o2  19787  gsumzres  20123  gsumzaddlem  20135  gsumzadd  20136  gsum2dlem2  20185  dprdfadd  20236  dprdres  20244  dprd2dlem1  20257  dprd2da  20258  lindfres  22129  opsrtoslem2  22365  txss12  23924  txbasval  23925  fmss  24265  ustneism  24543  trust  24548  isngp2  24916  equivcau  25621  metsscmetcld  25636  volf  25850  dvcnvrelem1  26337  pserdv  26756  dvlog  26979  dchrelbas2  27564  issubgr2  29853  subgrprop2  29855  uhgrspansubgr  29872  hlimadd  31795  hlimcaui  31838  hhssabloilem  31863  hhsst  31868  hhsssh2  31872  hhsscms  31880  occllem  31905  nlelchi  32663  hmopidmchi  32753  fnresin  33218  fressupp  33281  pfxrn2  33507  omsmon  34930  carsggect  34950  eulerpartlemmf  35007  funpartss  36708  brresi2  38654  bnd2lem  38725  idresssidinxp  39246  disjimres  39782  aks6d1c2  43180  eqresfnbd  43286  diophrw  43769  dnnumch2  44051  lmhmlnmsplit  44088  hbtlem6  44130  dfrcl2  44673  relexpaddss  44717  cotrclrcl  44741  frege131d  44763  resimass  46251  fourierdlem42  47158  fourierdlem80  47195  isubgredgss  48962  isubgrsubgr  48966  setrecsres  50794