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

Theorem resex 5892
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 5891 . 2 (𝐴 ∈ V → (𝐴𝐵) ∈ V)
31, 2ax-mp 5 1 (𝐴𝐵) ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  Vcvv 3492  cres 5550
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494  df-in 3940  df-ss 3949  df-res 5560
This theorem is referenced by:  wfrlem17  7960  tfrlem9a  8011  domunsncan  8605  sbthlem10  8624  mapunen  8674  php3  8691  ssfi  8726  marypha1lem  8885  infdifsn  9108  ackbij2lem3  9651  fin1a2lem7  9816  hashf1lem2  13802  ramub2  16338  resf1st  17152  resf2nd  17153  funcres  17154  lubfval  17576  glbfval  17589  znval  20610  znle  20611  uhgrspanop  27005  upgrspanop  27006  umgrspanop  27007  usgrspanop  27008  uhgrspan1lem1  27009  vtxdginducedm1lem1  27248  vtxdginducedm1fi  27253  finsumvtxdg2ssteplem4  27257  finsumvtxdg2size  27259  wlksnwwlknvbij  27614  clwwlkvbij  27819  eupthvdres  27941  eupth2lem3  27942  eupth2lemb  27943  hhssva  28961  hhsssm  28962  hhssnm  28963  hhshsslem1  28971  eulerpartlemt  31528  eulerpartgbij  31529  eulerpart  31539  fibp1  31558  actfunsnf1o  31774  subfacp1lem3  32326  subfacp1lem5  32328  dfrdg2  32937  dfrecs2  33308  finixpnum  34758  poimirlem4  34777  poimirlem9  34782  mbfresfi  34819  sdclem2  34898  diophrex  39250  rexrabdioph  39269  2rexfrabdioph  39271  3rexfrabdioph  39272  4rexfrabdioph  39273  6rexfrabdioph  39274  7rexfrabdioph  39275  rmydioph  39489  rmxdioph  39491  expdiophlem2  39497  ssnnf1octb  41332  dvnprodlem1  42107  dvnprodlem2  42108  fouriersw  42393  vonval  42699  hoidmvlelem2  42755  hoidmvlelem3  42756  iccelpart  43470
  Copyright terms: Public domain W3C validator