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

Theorem resex 5583
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 5582 . 2 (𝐴 ∈ V → (𝐴𝐵) ∈ V)
31, 2ax-mp 5 1 (𝐴𝐵) ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2145  Vcvv 3351  cres 5252
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-in 3730  df-ss 3737  df-res 5262
This theorem is referenced by:  wfrlem17  7588  tfrlem9a  7639  domunsncan  8220  sbthlem10  8239  mapunen  8289  php3  8306  ssfi  8340  marypha1lem  8499  infdifsn  8722  ackbij2lem3  9269  fin1a2lem7  9434  hashf1lem2  13442  ramub2  15925  resf1st  16761  resf2nd  16762  funcres  16763  lubfval  17186  glbfval  17199  znval  20098  znle  20099  uhgrspanop  26411  upgrspanop  26412  umgrspanop  26413  usgrspanop  26414  uhgrspan1lem1  26415  vtxdginducedm1lem1  26670  vtxdginducedm1fi  26675  finsumvtxdg2ssteplem4  26679  finsumvtxdg2size  26681  wlksnwwlknvbij  27052  wlksnwwlknvbijOLD  27053  clwwlkvbij  27289  clwwlkvbijOLDOLD  27290  clwwlkvbijOLD  27291  eupthvdres  27415  eupth2lem3  27416  eupth2lemb  27417  hhssva  28454  hhsssm  28455  hhssnm  28456  hhshsslem1  28464  eulerpartlemt  30773  eulerpartgbij  30774  eulerpart  30784  fibp1  30803  actfunsnf1o  31022  subfacp1lem3  31502  subfacp1lem5  31504  dfrdg2  32037  dfrecs2  32394  finixpnum  33726  poimirlem4  33745  poimirlem9  33750  mbfresfi  33787  sdclem2  33868  diophrex  37863  rexrabdioph  37882  2rexfrabdioph  37884  3rexfrabdioph  37885  4rexfrabdioph  37886  6rexfrabdioph  37887  7rexfrabdioph  37888  rmydioph  38105  rmxdioph  38107  expdiophlem2  38113  ssnnf1octb  39899  dvnprodlem1  40674  dvnprodlem2  40675  fouriersw  40960  vonval  41269  hoidmvlelem2  41325  hoidmvlelem3  41326  iccelpart  41892
  Copyright terms: Public domain W3C validator