Theorem resex 6003

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

Syntax hints:   ∈ wcel 2109  Vcvv 3450   ↾ cres 5643

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-in 3924  df-ss 3934  df-res 5653

This theorem is referenced by:  fprresex  8292  dfrecs3  8344  tfrlem9a  8357  domssl  8972  undom  9033  domunsncan  9046  sbthlem10  9066  mapunen  9116  dif1en  9130  dif1enOLD  9132  ssfiALT  9144  sbthfilem  9168  php3  9179  marypha1lem  9391  infdifsn  9617  ttrclss  9680  ackbij2lem3  10200  fin1a2lem7  10366  hashf1lem2  14428  ramub2  16992  resf1st  17863  resf2nd  17864  funcres  17865  lubfval  18316  glbfval  18329  znval  21452  znle  21453  uhgrspanop  29230  upgrspanop  29231  umgrspanop  29232  usgrspanop  29233  uhgrspan1lem1  29234  vtxdginducedm1lem1  29474  vtxdginducedm1fi  29479  finsumvtxdg2ssteplem4  29483  finsumvtxdg2size  29485  wlksnwwlknvbij  29845  clwwlkvbij  30049  eupthvdres  30171  eupth2lem3  30172  eupth2lemb  30173  hhssva  31193  hhsssm  31194  hhssnm  31195  hhshsslem1  31203  eulerpartlemt  34369  eulerpartgbij  34370  eulerpart  34380  fibp1  34399  actfunsnf1o  34602  subfacp1lem3  35176  subfacp1lem5  35178  dfrdg2  35790  dfrecs2  35945  finixpnum  37606  poimirlem4  37625  poimirlem9  37630  mbfresfi  37667  sdclem2  37743  diophrex  42770  rexrabdioph  42789  2rexfrabdioph  42791  3rexfrabdioph  42792  4rexfrabdioph  42793  6rexfrabdioph  42794  7rexfrabdioph  42795  rmydioph  43010  rmxdioph  43012  expdiophlem2  43018  ssnnf1octb  45195  dvnprodlem1  45951  dvnprodlem2  45952  fouriersw  46236  vonval  46545  hoidmvlelem2  46601  hoidmvlelem3  46602  iccelpart  47438  uhgrimisgrgric  47935