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

Theorem resexg 5161
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 5146 . 2  |-  ( A  |`  B )  C_  A
2 ssexg 4450 . 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 1756   _Vcvv 2984    C_ wss 3340    |` cres 4854
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4425
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2986  df-in 3347  df-ss 3354  df-res 4864
This theorem is referenced by:  resex  5162  fvtresfn  5787  offres  6584  ressuppss  6720  ressuppssdif  6722  resixp  7310  fsuppres  7657  climres  13065  setsvalg  14209  setsid  14227  symgfixels  15951  symgfixfvh  15953  gsumval3OLD  16394  gsumval3lem1  16395  gsumval3lem2  16396  gsum2dlem2  16474  gsum2dOLD  16476  qtopres  19283  tsmspropd  19714  ulmss  21874  uhgrares  23254  umgrares  23270  usgrares  23300  usgrares1  23335  cusgrares  23392  redwlk  23517  hhssva  24672  hhsssm  24673  hhshsslem1  24680  resf1o  26042  eulerpartlemmf  26770  exidres  28755  exidresid  28756  lmhmlnmsplit  29452  pwssplit4  29454
  Copyright terms: Public domain W3C validator