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

Theorem resex 5126
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 5125 . 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 1717   _Vcvv 2899    |` cres 4820
This theorem is referenced by:  tfrlem9a  6583  domunsncan  7144  sbthlem10  7162  mapunen  7212  php3  7229  ssfi  7265  marypha1lem  7373  infdifsn  7544  ackbij2lem3  8054  fin1a2lem7  8219  hashf1lem2  11632  ramub2  13309  resf1st  14018  resf2nd  14019  funcres  14020  znval  16739  znle  16740  usgrafis  21295  cusgrasize  21353  hhssva  22607  hhsssm  22608  hhssnm  22609  hhshsslem1  22615  subfacp1lem3  24647  subfacp1lem5  24649  dfrdg2  25176  nofulllem5  25384  tfrqfree  25514  sdclem2  26137  diophrex  26525  rexrabdioph  26545  2rexfrabdioph  26547  3rexfrabdioph  26548  4rexfrabdioph  26549  6rexfrabdioph  26550  7rexfrabdioph  26551  rmydioph  26776  rmxdioph  26778  expdiophlem2  26784
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-v 2901  df-in 3270  df-ss 3277  df-res 4830
  Copyright terms: Public domain W3C validator