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

Theorem resexg 5162
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 5143 . 2  |-  ( A  |`  B )  C_  A
2 ssexg 4566 . 2  |-  ( ( ( A  |`  B ) 
C_  A  /\  A  e.  V )  ->  ( A  |`  B )  e. 
_V )
31, 2mpan 674 1  |-  ( A  e.  V  ->  ( A  |`  B )  e. 
_V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1868   _Vcvv 3081    C_ wss 3436    |` cres 4851
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-v 3083  df-in 3443  df-ss 3450  df-res 4861
This theorem is referenced by:  resex  5163  fvtresfn  5962  offres  6798  ressuppss  6941  ressuppssdif  6943  resixp  7561  fsuppres  7910  climres  13624  setsvalg  15130  setsid  15149  symgfixels  17060  gsumval3lem1  17524  gsumval3lem2  17525  gsum2dlem2  17588  qtopres  20697  tsmspropd  21130  ulmss  23336  uhgrares  25019  umgrares  25035  usgrares  25080  usgrares1  25121  cusgrares  25183  redwlk  25319  hhssva  26893  hhsssm  26894  hhshsslem1  26901  resf1o  28306  eulerpartlemmf  29201  exidres  32087  exidresid  32088  lmhmlnmsplit  35862  pwssplit4  35864
  Copyright terms: Public domain W3C validator