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

Theorem resss 5342
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 5050 . 2 (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
2 inss1 3795 . 2 (𝐴 ∩ (𝐵 × V)) ⊆ 𝐴
31, 2eqsstri 3598 1 (𝐴𝐵) ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  Vcvv 3173  cin 3539  wss 3540   × cxp 5036  cres 5040
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554  df-res 5050
This theorem is referenced by:  relssres  5357  resexg  5362  iss  5367  mptss  5373  relresfld  5579  funres  5843  funres11  5880  funcnvres  5881  2elresin  5916  fssres  5983  foimacnv  6067  frxp  7174  fnwelem  7179  tposss  7240  dftpos4  7258  smores  7336  smores2  7338  tfrlem15  7375  finresfin  8071  fidomdm  8128  imafi  8142  marypha1lem  8222  hartogslem1  8330  r0weon  8718  ackbij2lem3  8946  axdc3lem2  9156  smobeth  9287  wunres  9432  vdwnnlem1  15537  symgsssg  17710  symgfisg  17711  psgnunilem5  17737  odf1o2  17811  gsumzres  18133  gsumzaddlem  18144  gsumzadd  18145  gsum2dlem2  18193  dprdfadd  18242  dprdres  18250  dprd2dlem1  18263  dprd2da  18264  opsrtoslem2  19306  lindfres  19981  txss12  21218  txbasval  21219  fmss  21560  ustneism  21837  trust  21843  isngp2  22211  equivcau  22906  cmetss  22921  volf  23104  dvcnvrelem1  23584  tdeglem4  23624  pserdv  23987  dvlog  24197  dchrelbas2  24762  uhgrares  25837  umgrares  25853  usgrares  25898  hlimadd  27434  hlimcaui  27477  hhssabloilem  27502  hhsst  27507  hhsssh2  27511  hhsscms  27520  occllem  27546  nlelchi  28304  hmopidmchi  28394  fnresin  28812  imafi2  28872  dmct  28877  omsmon  29687  carsggect  29707  eulerpartlemmf  29764  nodenselem6  31085  funpartss  31221  brresi  32683  bnd2lem  32760  diophrw  36340  dnnumch2  36633  lmhmlnmsplit  36675  hbtlem6  36718  dfrcl2  36985  relexpaddss  37029  cotrclrcl  37053  frege131d  37075  rnresss  38360  fourierdlem42  39042  fourierdlem80  39079  resisresindm  40320  issubgr2  40496  subgrprop2  40498  uhgrspansubgr  40515
  Copyright terms: Public domain W3C validator