Theorem resex 5928

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

Step	Hyp	Ref	Expression
1		resex.1	. 2 ⊢ 𝐴 ∈ V
2		resexg 5926	. 2 ⊢ (𝐴 ∈ V → (𝐴 ↾ 𝐵) ∈ V)
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ↾ 𝐵) ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3422   ↾ cres 5582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900  df-res 5592

This theorem is referenced by:  fprresex  8097  dfwrecsOLD  8100  wfrlem17OLD  8127  dfrecs3  8174  tfrlem9a  8188  domunsncan  8812  sbthlem10  8832  mapunen  8882  php3  8899  dif1en  8907  ssfiALT  8919  sbthfilem  8941  marypha1lem  9122  infdifsn  9345  ackbij2lem3  9928  fin1a2lem7  10093  hashf1lem2  14098  ramub2  16643  resf1st  17525  resf2nd  17526  funcres  17527  lubfval  17983  glbfval  17996  znval  20651  znle  20652  uhgrspanop  27566  upgrspanop  27567  umgrspanop  27568  usgrspanop  27569  uhgrspan1lem1  27570  vtxdginducedm1lem1  27809  vtxdginducedm1fi  27814  finsumvtxdg2ssteplem4  27818  finsumvtxdg2size  27820  wlksnwwlknvbij  28174  clwwlkvbij  28378  eupthvdres  28500  eupth2lem3  28501  eupth2lemb  28502  hhssva  29520  hhsssm  29521  hhssnm  29522  hhshsslem1  29530  eulerpartlemt  32238  eulerpartgbij  32239  eulerpart  32249  fibp1  32268  actfunsnf1o  32484  subfacp1lem3  33044  subfacp1lem5  33046  dfrdg2  33677  ttrclss  33706  dfrecs2  34179  finixpnum  35689  poimirlem4  35708  poimirlem9  35713  mbfresfi  35750  sdclem2  35827  diophrex  40513  rexrabdioph  40532  2rexfrabdioph  40534  3rexfrabdioph  40535  4rexfrabdioph  40536  6rexfrabdioph  40537  7rexfrabdioph  40538  rmydioph  40752  rmxdioph  40754  expdiophlem2  40760  ssnnf1octb  42622  dvnprodlem1  43377  dvnprodlem2  43378  fouriersw  43662  vonval  43968  hoidmvlelem2  44024  hoidmvlelem3  44025  iccelpart  44773