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

Theorem resex 5478
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 5477 . 2 (𝐴 ∈ V → (𝐴𝐵) ∈ V)
31, 2ax-mp 5 1 (𝐴𝐵) ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2030  Vcvv 3231  cres 5145
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-in 3614  df-ss 3621  df-res 5155
This theorem is referenced by:  wfrlem17  7476  tfrlem9a  7527  domunsncan  8101  sbthlem10  8120  mapunen  8170  php3  8187  ssfi  8221  marypha1lem  8380  infdifsn  8592  ackbij2lem3  9101  fin1a2lem7  9266  hashf1lem2  13278  ramub2  15765  resf1st  16601  resf2nd  16602  funcres  16603  lubfval  17025  glbfval  17038  znval  19931  znle  19932  uhgrspanop  26233  upgrspanop  26234  umgrspanop  26235  usgrspanop  26236  uhgrspan1lem1  26237  vtxdginducedm1lem1  26491  vtxdginducedm1fi  26496  finsumvtxdg2ssteplem4  26500  finsumvtxdg2size  26502  wlksnwwlknvbij  26871  clwwlkvbij  27088  clwwlkvbijOLD  27089  eupthvdres  27213  eupth2lem3  27214  eupth2lemb  27215  hhssva  28242  hhsssm  28243  hhssnm  28244  hhshsslem1  28252  eulerpartlemt  30561  eulerpartgbij  30562  eulerpart  30572  fibp1  30591  actfunsnf1o  30810  subfacp1lem3  31290  subfacp1lem5  31292  dfrdg2  31825  dfrecs2  32182  finixpnum  33524  poimirlem4  33543  poimirlem9  33548  mbfresfi  33586  sdclem2  33668  diophrex  37656  rexrabdioph  37675  2rexfrabdioph  37677  3rexfrabdioph  37678  4rexfrabdioph  37679  6rexfrabdioph  37680  7rexfrabdioph  37681  rmydioph  37898  rmxdioph  37900  expdiophlem2  37906  ssnnf1octb  39696  dvnprodlem1  40479  dvnprodlem2  40480  fouriersw  40766  vonval  41075  hoidmvlelem2  41131  hoidmvlelem3  41132  iccelpart  41694
  Copyright terms: Public domain W3C validator