Theorem resex 6016

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 6014	. 2 ⊢ (𝐴 ∈ V → (𝐴 ↾ 𝐵) ∈ V)
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ↾ 𝐵) ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3459   ↾ cres 5656

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-in 3933  df-ss 3943  df-res 5666

This theorem is referenced by:  fprresex  8309  dfwrecsOLD  8312  wfrlem17OLD  8339  dfrecs3  8386  tfrlem9a  8400  domssl  9012  undom  9073  domunsncan  9086  sbthlem10  9106  mapunen  9160  dif1en  9174  dif1enOLD  9176  ssfiALT  9188  sbthfilem  9212  php3  9223  php3OLD  9233  marypha1lem  9445  infdifsn  9671  ttrclss  9734  ackbij2lem3  10254  fin1a2lem7  10420  hashf1lem2  14474  ramub2  17034  resf1st  17907  resf2nd  17908  funcres  17909  lubfval  18360  glbfval  18373  znval  21496  znle  21497  uhgrspanop  29275  upgrspanop  29276  umgrspanop  29277  usgrspanop  29278  uhgrspan1lem1  29279  vtxdginducedm1lem1  29519  vtxdginducedm1fi  29524  finsumvtxdg2ssteplem4  29528  finsumvtxdg2size  29530  wlksnwwlknvbij  29890  clwwlkvbij  30094  eupthvdres  30216  eupth2lem3  30217  eupth2lemb  30218  hhssva  31238  hhsssm  31239  hhssnm  31240  hhshsslem1  31248  eulerpartlemt  34403  eulerpartgbij  34404  eulerpart  34414  fibp1  34433  actfunsnf1o  34636  subfacp1lem3  35204  subfacp1lem5  35206  dfrdg2  35813  dfrecs2  35968  finixpnum  37629  poimirlem4  37648  poimirlem9  37653  mbfresfi  37690  sdclem2  37766  diophrex  42798  rexrabdioph  42817  2rexfrabdioph  42819  3rexfrabdioph  42820  4rexfrabdioph  42821  6rexfrabdioph  42822  7rexfrabdioph  42823  rmydioph  43038  rmxdioph  43040  expdiophlem2  43046  ssnnf1octb  45218  dvnprodlem1  45975  dvnprodlem2  45976  fouriersw  46260  vonval  46569  hoidmvlelem2  46625  hoidmvlelem3  46626  iccelpart  47447  uhgrimisgrgric  47944