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

Theorem resex 5145
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 5144 . 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 1721   _Vcvv 2916    |` cres 4839
This theorem is referenced by:  tfrlem9a  6606  domunsncan  7167  sbthlem10  7185  mapunen  7235  php3  7252  ssfi  7288  marypha1lem  7396  infdifsn  7567  ackbij2lem3  8077  fin1a2lem7  8242  hashf1lem2  11660  ramub2  13337  resf1st  14046  resf2nd  14047  funcres  14048  znval  16771  znle  16772  usgrafis  21382  cusgrasize  21440  hhssva  22712  hhsssm  22713  hhssnm  22714  hhshsslem1  22720  subfacp1lem3  24821  subfacp1lem5  24823  dfrdg2  25366  nofulllem5  25574  tfrqfree  25704  mbfresfi  26152  sdclem2  26336  diophrex  26724  rexrabdioph  26744  2rexfrabdioph  26746  3rexfrabdioph  26747  4rexfrabdioph  26748  6rexfrabdioph  26749  7rexfrabdioph  26750  rmydioph  26975  rmxdioph  26977  expdiophlem2  26983
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-in 3287  df-ss 3294  df-res 4849
  Copyright terms: Public domain W3C validator