MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  resexg Unicode version

Theorem resexg 5321
Description: The restriction of a set is a set. (Contributed by NM, 28-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
Assertion
Ref Expression
resexg

Proof of Theorem resexg
StepHypRef Expression
1 resss 5302 . 2
2 ssexg 4598 . 2
31, 2mpan 670 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818   cvv 3109  C_wss 3475  |`cres 5006
This theorem is referenced by:  resex  5322  fvtresfn  5957  offres  6795  ressuppss  6938  ressuppssdif  6940  resixp  7524  fsuppres  7874  climres  13398  setsvalg  14655  setsid  14673  symgfixels  16459  gsumval3OLD  16908  gsumval3lem1  16909  gsumval3lem2  16910  gsum2dlem2  16998  gsum2dOLD  17000  qtopres  20199  tsmspropd  20630  ulmss  22792  uhgrares  24308  umgrares  24324  usgrares  24369  usgrares1  24410  cusgrares  24472  redwlk  24608  hhssva  26175  hhsssm  26176  hhshsslem1  26183  resf1o  27553  eulerpartlemmf  28314  exidres  30340  exidresid  30341  lmhmlnmsplit  31033  pwssplit4  31035
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3482  df-ss 3489  df-res 5016
  Copyright terms: Public domain W3C validator