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

Theorem resexg 5316
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 5297 . 2  |-  ( A  |`  B )  C_  A
2 ssexg 4593 . 2  |-  ( ( ( A  |`  B ) 
C_  A  /\  A  e.  V )  ->  ( A  |`  B )  e. 
_V )
31, 2mpan 670 1  |-  ( A  e.  V  ->  ( A  |`  B )  e. 
_V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767   _Vcvv 3113    C_ wss 3476    |` cres 5001
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483  df-ss 3490  df-res 5011
This theorem is referenced by:  resex  5317  fvtresfn  5951  offres  6779  ressuppss  6919  ressuppssdif  6921  resixp  7504  fsuppres  7854  climres  13361  setsvalg  14513  setsid  14531  symgfixels  16264  symgfixfvh  16266  gsumval3OLD  16711  gsumval3lem1  16712  gsumval3lem2  16713  gsum2dlem2  16801  gsum2dOLD  16803  qtopres  19962  tsmspropd  20393  ulmss  22554  uhgrares  24012  umgrares  24028  usgrares  24073  usgrares1  24114  cusgrares  24176  redwlk  24312  hhssva  25879  hhsssm  25880  hhshsslem1  25887  resf1o  27253  eulerpartlemmf  27982  exidres  29971  exidresid  29972  lmhmlnmsplit  30665  pwssplit4  30667
  Copyright terms: Public domain W3C validator