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

Theorem resexg 5152
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 5137 . 2  |-  ( A  |`  B )  C_  A
2 ssexg 4317 . 2  |-  ( ( ( A  |`  B ) 
C_  A  /\  A  e.  V )  ->  ( A  |`  B )  e. 
_V )
31, 2mpan 652 1  |-  ( A  e.  V  ->  ( A  |`  B )  e. 
_V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   _Vcvv 2924    C_ wss 3288    |` cres 4847
This theorem is referenced by:  resex  5153  offres  6286  resixp  7064  climres  12332  setsvalg  13455  setsid  13471  gsumval3  15477  gsum2d  15509  qtopres  17691  tsmspropd  18122  ulmss  20274  uhgrares  21304  umgrares  21320  usgrares  21350  usgrares1  21385  cusgrares  21442  redwlk  21567  hhssva  22720  hhsssm  22721  hhshsslem1  22728  exidres  26451  exidresid  26452  fvtresfn  26642  lmhmlnmsplit  27061  pwssplit4  27067
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-sep 4298
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-v 2926  df-in 3295  df-ss 3302  df-res 4857
  Copyright terms: Public domain W3C validator