Theorem resss 5958

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

Syntax hints:  Vcvv 3438   ∩ cin 3898   ⊆ wss 3899   × cxp 5620   ↾ cres 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-in 3906  df-ss 3916  df-res 5634

This theorem is referenced by:  dmresss  5968  rnresss  5974  relssres  5979  resexg  5984  iss  5992  mptss  5999  relresfld  6232  funres  6532  funres11  6567  funcnvres  6568  2elresin  6611  fssres  6698  foimacnv  6789  frxp  8066  fnwelem  8071  tposss  8167  dftpos4  8185  smores  8282  smores2  8284  tfrlem15  8321  finresfin  9170  imafi  9213  fidomdm  9232  imafi2  9259  marypha1lem  9334  hartogslem1  9445  r0weon  9920  ackbij2lem3  10148  axdc3lem2  10359  dmct  10432  smobeth  10495  wunres  10640  vdwnnlem1  16921  symgsssg  19394  symgfisg  19395  psgnunilem5  19421  odf1o2  19500  gsumzres  19836  gsumzaddlem  19848  gsumzadd  19849  gsum2dlem2  19898  dprdfadd  19949  dprdres  19957  dprd2dlem1  19970  dprd2da  19971  lindfres  21776  opsrtoslem2  22009  txss12  23547  txbasval  23548  fmss  23888  ustneism  24166  trust  24171  isngp2  24539  equivcau  25254  metsscmetcld  25269  volf  25484  dvcnvrelem1  25976  pserdv  26393  dvlog  26614  dchrelbas2  27202  issubgr2  29294  subgrprop2  29296  uhgrspansubgr  29313  hlimadd  31217  hlimcaui  31260  hhssabloilem  31285  hhsst  31290  hhsssh2  31294  hhsscms  31302  occllem  31327  nlelchi  32085  hmopidmchi  32175  fnresin  32651  fressupp  32716  pfxrn2  32971  omsmon  34404  carsggect  34424  eulerpartlemmf  34481  funpartss  36087  brresi2  37860  bnd2lem  37931  idresssidinxp  38446  disjimres  38948  aks6d1c2  42323  eqresfnbd  42430  diophrw  42943  dnnumch2  43229  lmhmlnmsplit  43271  hbtlem6  43313  dfrcl2  43857  relexpaddss  43901  cotrclrcl  43925  frege131d  43947  resimass  45426  fourierdlem42  46335  fourierdlem80  46372  isubgredgss  48053  isubgrsubgr  48057  setrecsres  49889