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

Theorem resex 5168
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 5167 . 2  |-  ( A  e.  _V  ->  ( A  |`  B )  e. 
_V )
31, 2ax-mp 5 1  |-  ( A  |`  B )  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1870   _Vcvv 3087    |` cres 4856
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 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-in 3449  df-ss 3456  df-res 4866
This theorem is referenced by:  wfrlem17  7060  tfrlem9a  7112  domunsncan  7678  sbthlem10  7697  mapunen  7747  php3  7764  ssfi  7798  marypha1lem  7953  infdifsn  8161  ackbij2lem3  8669  fin1a2lem7  8834  hashf1lem2  12614  ramub2  14925  resf1st  15741  resf2nd  15742  funcres  15743  lubfval  16166  glbfval  16179  znval  19028  znle  19029  usgrafis  24979  cusgrasize  25042  wlknwwlknvbij  25304  clwwlkvbij  25365  hhssva  26736  hhsssm  26737  hhssnm  26738  hhshsslem1  26744  eulerpartlemt  29021  eulerpartgbij  29022  eulerpart  29032  fibp1  29051  subfacp1lem3  29684  subfacp1lem5  29686  dfrdg2  30220  nofulllem5  30371  dfrecs2  30493  finixpnum  31624  poimirlem4  31638  poimirlem9  31643  mbfresfi  31681  sdclem2  31765  diophrex  35317  rexrabdioph  35336  2rexfrabdioph  35338  3rexfrabdioph  35339  4rexfrabdioph  35340  6rexfrabdioph  35341  7rexfrabdioph  35342  rmydioph  35565  rmxdioph  35567  expdiophlem2  35573  dvnprodlem1  37380  dvnprodlem2  37381  fouriersw  37653  iccelpart  38127  uhgres  38439
  Copyright terms: Public domain W3C validator