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

Theorem resexg 5010
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  |-  ( A  e.  V  ->  ( A  |`  B )  e. 
_V )

Proof of Theorem resexg
StepHypRef Expression
1 resss 4995 . 2  |-  ( A  |`  B )  C_  A
2 ssexg 4176 . 2  |-  ( ( ( A  |`  B ) 
C_  A  /\  A  e.  V )  ->  ( A  |`  B )  e. 
_V )
31, 2mpan 651 1  |-  ( A  e.  V  ->  ( A  |`  B )  e. 
_V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696   _Vcvv 2801    C_ wss 3165    |` cres 4707
This theorem is referenced by:  resex  5011  offres  6108  resixp  6867  climres  12065  setsvalg  13187  setsid  13203  gsumval3  15207  gsum2d  15239  qtopres  17405  tsmspropd  17830  ulmss  19790  hhssva  21852  hhsssm  21853  hhshsslem1  21860  umgrares  23891  exidres  26671  exidresid  26672  fvtresfn  26866  lmhmlnmsplit  27288  pwssplit4  27294  usgrares  28249  redwlk  28364
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-ss 3179  df-res 4717
  Copyright terms: Public domain W3C validator