Theorem resex 5899

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

Syntax hints:   ∈ wcel 2110  Vcvv 3408   ↾ cres 5553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708  ax-sep 5192

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070  df-v 3410  df-in 3873  df-ss 3883  df-res 5563

This theorem is referenced by:  wfrlem17  8071  tfrlem9a  8122  domunsncan  8745  sbthlem10  8765  mapunen  8815  php3  8832  dif1en  8840  ssfiALT  8852  marypha1lem  9049  infdifsn  9272  ackbij2lem3  9855  fin1a2lem7  10020  hashf1lem2  14022  ramub2  16567  resf1st  17400  resf2nd  17401  funcres  17402  lubfval  17856  glbfval  17869  znval  20500  znle  20501  uhgrspanop  27384  upgrspanop  27385  umgrspanop  27386  usgrspanop  27387  uhgrspan1lem1  27388  vtxdginducedm1lem1  27627  vtxdginducedm1fi  27632  finsumvtxdg2ssteplem4  27636  finsumvtxdg2size  27638  wlksnwwlknvbij  27992  clwwlkvbij  28196  eupthvdres  28318  eupth2lem3  28319  eupth2lemb  28320  hhssva  29338  hhsssm  29339  hhssnm  29340  hhshsslem1  29348  eulerpartlemt  32050  eulerpartgbij  32051  eulerpart  32061  fibp1  32080  actfunsnf1o  32296  subfacp1lem3  32857  subfacp1lem5  32859  dfrdg2  33490  ttrclss  33519  dfrecs2  33989  finixpnum  35499  poimirlem4  35518  poimirlem9  35523  mbfresfi  35560  sdclem2  35637  diophrex  40300  rexrabdioph  40319  2rexfrabdioph  40321  3rexfrabdioph  40322  4rexfrabdioph  40323  6rexfrabdioph  40324  7rexfrabdioph  40325  rmydioph  40539  rmxdioph  40541  expdiophlem2  40547  ssnnf1octb  42406  dvnprodlem1  43162  dvnprodlem2  43163  fouriersw  43447  vonval  43753  hoidmvlelem2  43809  hoidmvlelem3  43810  iccelpart  44558