MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  resss Structured version   Visualization version   GIF version

Theorem resss 5410
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
StepHypRef Expression
1 df-res 5116 . 2 (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
2 inss1 3825 . 2 (𝐴 ∩ (𝐵 × V)) ⊆ 𝐴
31, 2eqsstri 3627 1 (𝐴𝐵) ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  Vcvv 3195  cin 3566  wss 3567   × cxp 5102  cres 5106
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-in 3574  df-ss 3581  df-res 5116
This theorem is referenced by:  relssres  5425  resexg  5430  iss  5435  mptss  5442  relresfld  5650  funres  5917  funres11  5954  funcnvres  5955  2elresin  5990  fssres  6057  foimacnv  6141  frxp  7272  fnwelem  7277  tposss  7338  dftpos4  7356  smores  7434  smores2  7436  tfrlem15  7473  finresfin  8171  fidomdm  8228  imafi  8244  marypha1lem  8324  hartogslem1  8432  r0weon  8820  ackbij2lem3  9048  axdc3lem2  9258  dmct  9331  smobeth  9393  wunres  9538  vdwnnlem1  15680  symgsssg  17868  symgfisg  17869  psgnunilem5  17895  odf1o2  17969  gsumzres  18291  gsumzaddlem  18302  gsumzadd  18303  gsum2dlem2  18351  dprdfadd  18400  dprdres  18408  dprd2dlem1  18421  dprd2da  18422  opsrtoslem2  19466  lindfres  20143  txss12  21389  txbasval  21390  fmss  21731  ustneism  22008  trust  22014  isngp2  22382  equivcau  23079  cmetss  23094  volf  23278  dvcnvrelem1  23761  tdeglem4  23801  pserdv  24164  dvlog  24378  dchrelbas2  24943  issubgr2  26145  subgrprop2  26147  uhgrspansubgr  26164  hlimadd  28020  hlimcaui  28063  hhssabloilem  28088  hhsst  28093  hhsssh2  28097  hhsscms  28106  occllem  28132  nlelchi  28890  hmopidmchi  28980  fnresin  29403  imafi2  29463  omsmon  30334  carsggect  30354  eulerpartlemmf  30411  funpartss  32026  brresi  33484  bnd2lem  33561  diophrw  37141  dnnumch2  37434  lmhmlnmsplit  37476  hbtlem6  37518  dfrcl2  37785  relexpaddss  37829  cotrclrcl  37853  frege131d  37875  rnresss  39181  resimass  39265  fourierdlem42  40129  fourierdlem80  40166
  Copyright terms: Public domain W3C validator