Theorem resss 5994

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

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

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 3906  df-ss 3916  df-res 5667

This theorem is used by:  dmresss  6004  rnresss  6010  relssres  6015  resexg  6020  iss  6031  mptss  6038  cnvcnvss  6187  relresfldOLD  6274  funres  6576  funres11  6611  funcnvres  6612  2elresin  6654  fssres  6742  foimacnv  6836  frxp  8125  fnwelem  8130  tposss  8226  dftpos4  8244  smores  8342  smores2  8344  tfrlem15  8382  finresfin  9245  imafi  9288  fidomdm  9304  imafi2  9331  marypha1lem  9406  hartogslem1  9517  r0weon  10018  ackbij2lem3  10245  axdc3lem2  10456  dmct  10529  dmctOLD  10530  smobeth  10598  wunres  10743  vdwnnlem1  17090  symgsssg  19597  symgfisg  19598  psgnunilem5  19624  odf1o2  19703  gsumzres  20039  gsumzaddlem  20051  gsumzadd  20052  gsum2dlem2  20101  dprdfadd  20152  dprdres  20160  dprd2dlem1  20173  dprd2da  20174  lindfres  22039  opsrtoslem2  22275  txss12  23834  txbasval  23835  fmss  24175  ustneism  24453  trust  24458  isngp2  24826  equivcau  25531  metsscmetcld  25546  volf  25760  dvcnvrelem1  26247  pserdv  26668  dvlog  26891  dchrelbas2  27476  issubgr2  29735  subgrprop2  29737  uhgrspansubgr  29754  hlimadd  31677  hlimcaui  31720  hhssabloilem  31745  hhsst  31750  hhsssh2  31754  hhsscms  31762  occllem  31787  nlelchi  32545  hmopidmchi  32635  fnresin  33100  fressupp  33163  pfxrn2  33389  omsmon  34812  carsggect  34832  eulerpartlemmf  34889  funpartss  36526  brresi2  38473  bnd2lem  38544  idresssidinxp  39065  disjimres  39601  aks6d1c2  42999  eqresfnbd  43105  diophrw  43607  dnnumch2  43889  lmhmlnmsplit  43931  hbtlem6  43973  dfrcl2  44517  relexpaddss  44561  cotrclrcl  44585  frege131d  44607  resimass  46072  fourierdlem42  46980  fourierdlem80  47017  isubgredgss  48784  isubgrsubgr  48788  setrecsres  50631