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

Theorem resex 5655
Description: The restriction of a set is a set. (Contributed by Jeff Madsen, 19-Jun-2011.)
Hypothesis
Ref Expression
resex.1 𝐴 ∈ V
Assertion
Ref Expression
resex (𝐴𝐵) ∈ V

Proof of Theorem resex
StepHypRef Expression
1 resex.1 . 2 𝐴 ∈ V
2 resexg 5654 . 2 (𝐴 ∈ V → (𝐴𝐵) ∈ V)
31, 2ax-mp 5 1 (𝐴𝐵) ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2157  Vcvv 3385  cres 5314
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777  ax-sep 4975
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-v 3387  df-in 3776  df-ss 3783  df-res 5324
This theorem is referenced by:  wfrlem17  7670  tfrlem9a  7721  domunsncan  8302  sbthlem10  8321  mapunen  8371  php3  8388  ssfi  8422  marypha1lem  8581  infdifsn  8804  ackbij2lem3  9351  fin1a2lem7  9516  hashf1lem2  13489  ramub2  16051  resf1st  16868  resf2nd  16869  funcres  16870  lubfval  17293  glbfval  17306  znval  20205  znle  20206  uhgrspanop  26530  upgrspanop  26531  umgrspanop  26532  usgrspanop  26533  uhgrspan1lem1  26534  vtxdginducedm1lem1  26789  vtxdginducedm1fi  26794  finsumvtxdg2ssteplem4  26798  finsumvtxdg2size  26800  wlksnwwlknvbij  27188  wlksnwwlknvbijOLD  27189  clwwlkvbij  27453  clwwlkvbijOLD  27454  clwwlkvbijOLDOLD  27455  eupthvdres  27580  eupth2lem3  27581  eupth2lemb  27582  hhssva  28639  hhsssm  28640  hhssnm  28641  hhshsslem1  28649  eulerpartlemt  30949  eulerpartgbij  30950  eulerpart  30960  fibp1  30980  actfunsnf1o  31202  subfacp1lem3  31681  subfacp1lem5  31683  dfrdg2  32213  dfrecs2  32570  finixpnum  33883  poimirlem4  33902  poimirlem9  33907  mbfresfi  33944  sdclem2  34025  diophrex  38125  rexrabdioph  38144  2rexfrabdioph  38146  3rexfrabdioph  38147  4rexfrabdioph  38148  6rexfrabdioph  38149  7rexfrabdioph  38150  rmydioph  38366  rmxdioph  38368  expdiophlem2  38374  ssnnf1octb  40136  dvnprodlem1  40905  dvnprodlem2  40906  fouriersw  41191  vonval  41500  hoidmvlelem2  41556  hoidmvlelem3  41557  iccelpart  42209
  Copyright terms: Public domain W3C validator