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

Theorem resex 5250
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 5249 . 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 1758   _Vcvv 3070    |` cres 4942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4513
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-v 3072  df-in 3435  df-ss 3442  df-res 4952
This theorem is referenced by:  tfrlem9a  6947  domunsncan  7513  sbthlem10  7532  mapunen  7582  php3  7599  ssfi  7636  marypha1lem  7786  infdifsn  7965  ackbij2lem3  8513  fin1a2lem7  8678  hashf1lem2  12313  ramub2  14179  resf1st  14908  resf2nd  14909  funcres  14910  lubfval  15252  glbfval  15265  znval  18077  znle  18078  usgrafis  23465  cusgrasize  23523  hhssva  24797  hhsssm  24798  hhssnm  24799  hhshsslem1  24805  eulerpartlemt  26890  eulerpartgbij  26891  eulerpart  26901  fibp1  26920  subfacp1lem3  27206  subfacp1lem5  27208  dfrdg2  27745  nofulllem5  27983  tfrqfree  28118  finixpnum  28554  mbfresfi  28578  sdclem2  28778  diophrex  29254  rexrabdioph  29272  2rexfrabdioph  29274  3rexfrabdioph  29275  4rexfrabdioph  29276  6rexfrabdioph  29277  7rexfrabdioph  29278  rmydioph  29503  rmxdioph  29505  expdiophlem2  29511  wlknwwlknvbij  30512  clwwlkvbij  30603
  Copyright terms: Public domain W3C validator