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

Theorem resex 4995
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 4994 . 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 1684   _Vcvv 2788    |` cres 4691
This theorem is referenced by:  tfrlem9a  6402  domunsncan  6962  sbthlem10  6980  mapunen  7030  php3  7047  ssfi  7083  marypha1lem  7186  infdifsn  7357  ackbij2lem3  7867  fin1a2lem7  8032  hashf1lem2  11394  ramub2  13061  resf1st  13768  resf2nd  13769  funcres  13770  znval  16489  znle  16490  hhssva  21836  hhsssm  21837  hhssnm  21838  hhshsslem1  21844  subfacp1lem3  23713  subfacp1lem5  23715  dfrdg2  24152  nofulllem5  24360  tfrqfree  24489  prjmapcp2  25170  resexOLD  26382  sdclem2  26452  diophrex  26855  rexrabdioph  26875  2rexfrabdioph  26877  3rexfrabdioph  26878  4rexfrabdioph  26879  6rexfrabdioph  26880  7rexfrabdioph  26881  rmydioph  27107  rmxdioph  27109  expdiophlem2  27115
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ss 3166  df-res 4701
  Copyright terms: Public domain W3C validator