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

Theorem resex 5011
Description: The restriction of a set is a set. (Contributed by Jeff Madsen, 19-Jun-2011.)
Hypothesis
Ref Expression
resex.1  |-  A  e. 
_V
Assertion
Ref Expression
resex  |-  ( A  |`  B )  e.  _V

Proof of Theorem resex
StepHypRef Expression
1 resex.1 . 2  |-  A  e. 
_V
2 resexg 5010 . 2  |-  ( A  e.  _V  ->  ( A  |`  B )  e. 
_V )
31, 2ax-mp 8 1  |-  ( A  |`  B )  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1696   _Vcvv 2801    |` cres 4707
This theorem is referenced by:  tfrlem9a  6418  domunsncan  6978  sbthlem10  6996  mapunen  7046  php3  7063  ssfi  7099  marypha1lem  7202  infdifsn  7373  ackbij2lem3  7883  fin1a2lem7  8048  hashf1lem2  11410  ramub2  13077  resf1st  13784  resf2nd  13785  funcres  13786  znval  16505  znle  16506  hhssva  21852  hhsssm  21853  hhssnm  21854  hhshsslem1  21860  subfacp1lem3  23728  subfacp1lem5  23730  dfrdg2  24223  nofulllem5  24431  tfrqfree  24561  prjmapcp2  25273  resexOLD  26485  sdclem2  26555  diophrex  26958  rexrabdioph  26978  2rexfrabdioph  26980  3rexfrabdioph  26981  4rexfrabdioph  26982  6rexfrabdioph  26983  7rexfrabdioph  26984  rmydioph  27210  rmxdioph  27212  expdiophlem2  27218
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-ss 3179  df-res 4717
  Copyright terms: Public domain W3C validator