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

Theorem resex 5363
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 5362 . 2 (𝐴 ∈ V → (𝐴𝐵) ∈ V)
31, 2ax-mp 5 1 (𝐴𝐵) ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 1977  Vcvv 3173  cres 5040
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554  df-res 5050
This theorem is referenced by:  wfrlem17  7318  tfrlem9a  7369  domunsncan  7945  sbthlem10  7964  mapunen  8014  php3  8031  ssfi  8065  marypha1lem  8222  infdifsn  8437  ackbij2lem3  8946  fin1a2lem7  9111  hashf1lem2  13097  ramub2  15556  resf1st  16377  resf2nd  16378  funcres  16379  lubfval  16801  glbfval  16814  znval  19702  znle  19703  usgrafis  25944  cusgrasize  26006  wlknwwlknvbij  26268  clwwlkvbij  26329  hhssva  27498  hhsssm  27499  hhssnm  27500  hhshsslem1  27508  eulerpartlemt  29760  eulerpartgbij  29761  eulerpart  29771  fibp1  29790  subfacp1lem3  30418  subfacp1lem5  30420  dfrdg2  30945  nofulllem5  31105  dfrecs2  31227  finixpnum  32564  poimirlem4  32583  poimirlem9  32588  mbfresfi  32626  sdclem2  32708  diophrex  36357  rexrabdioph  36376  2rexfrabdioph  36378  3rexfrabdioph  36379  4rexfrabdioph  36380  6rexfrabdioph  36381  7rexfrabdioph  36382  rmydioph  36599  rmxdioph  36601  expdiophlem2  36607  ssnnf1octb  38377  dvnprodlem1  38836  dvnprodlem2  38837  fouriersw  39124  vonval  39430  hoidmvlelem2  39486  hoidmvlelem3  39487  iccelpart  39971  uhgrspanop  40520  upgrspanop  40521  umgrspanop  40522  usgrspanop  40523  uhgrspan1lem1  40524  wlksnwwlknvbij  41114  clwwlksvbij  41229  eupthvdres  41403  eupth2lem3  41404  eupth2lemb  41405
  Copyright terms: Public domain W3C validator