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

Theorem resexg 5303
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 5284 . 2  |-  ( A  |`  B )  C_  A
2 ssexg 4580 . 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 1802   _Vcvv 3093    C_ wss 3459    |` cres 4988
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4555
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-v 3095  df-in 3466  df-ss 3473  df-res 4998
This theorem is referenced by:  resex  5304  fvtresfn  5939  offres  6777  ressuppss  6918  ressuppssdif  6920  resixp  7503  fsuppres  7853  climres  13374  setsvalg  14529  setsid  14547  symgfixels  16330  gsumval3OLD  16779  gsumval3lem1  16780  gsumval3lem2  16781  gsum2dlem2  16869  gsum2dOLD  16871  qtopres  20069  tsmspropd  20500  ulmss  22661  uhgrares  24177  umgrares  24193  usgrares  24238  usgrares1  24279  cusgrares  24341  redwlk  24477  hhssva  26044  hhsssm  26045  hhshsslem1  26052  resf1o  27422  eulerpartlemmf  28184  exidres  30312  exidresid  30313  lmhmlnmsplit  31005  pwssplit4  31007
  Copyright terms: Public domain W3C validator