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

Theorem resex 5404
 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 5403 . 2 (𝐴 ∈ V → (𝐴𝐵) ∈ V)
31, 2ax-mp 5 1 (𝐴𝐵) ∈ V
 Colors of variables: wff setvar class Syntax hints:   ∈ wcel 1987  Vcvv 3186   ↾ cres 5078 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4743 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-in 3563  df-ss 3570  df-res 5088 This theorem is referenced by:  wfrlem17  7379  tfrlem9a  7430  domunsncan  8007  sbthlem10  8026  mapunen  8076  php3  8093  ssfi  8127  marypha1lem  8286  infdifsn  8501  ackbij2lem3  9010  fin1a2lem7  9175  hashf1lem2  13181  ramub2  15645  resf1st  16478  resf2nd  16479  funcres  16480  lubfval  16902  glbfval  16915  znval  19805  znle  19806  uhgrspanop  26088  upgrspanop  26089  umgrspanop  26090  usgrspanop  26091  uhgrspan1lem1  26092  wlksnwwlknvbij  26679  clwwlksvbij  26795  eupthvdres  26968  eupth2lem3  26969  eupth2lemb  26970  hhssva  27975  hhsssm  27976  hhssnm  27977  hhshsslem1  27985  eulerpartlemt  30226  eulerpartgbij  30227  eulerpart  30237  fibp1  30256  subfacp1lem3  30893  subfacp1lem5  30895  dfrdg2  31423  dfrecs2  31720  finixpnum  33047  poimirlem4  33066  poimirlem9  33071  mbfresfi  33109  sdclem2  33191  diophrex  36840  rexrabdioph  36859  2rexfrabdioph  36861  3rexfrabdioph  36862  4rexfrabdioph  36863  6rexfrabdioph  36864  7rexfrabdioph  36865  rmydioph  37082  rmxdioph  37084  expdiophlem2  37090  ssnnf1octb  38874  dvnprodlem1  39484  dvnprodlem2  39485  fouriersw  39771  vonval  40077  hoidmvlelem2  40133  hoidmvlelem3  40134  iccelpart  40683
 Copyright terms: Public domain W3C validator