Theorem resex 5986

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

Syntax hints:   ∈ wcel 2114  Vcvv 3430   ↾ cres 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-in 3897  df-ss 3907  df-res 5634

This theorem is referenced by:  fprresex  8251  dfrecs3  8303  tfrlem9a  8316  domssl  8936  undom  8994  domunsncan  9006  sbthlem10  9025  mapunen  9075  dif1en  9087  ssfiALT  9099  sbthfilem  9123  php3  9134  marypha1lem  9337  infdifsn  9567  ttrclss  9630  ackbij2lem3  10151  fin1a2lem7  10317  hashf1lem2  14380  ramub2  16943  resf1st  17819  resf2nd  17820  funcres  17821  lubfval  18272  glbfval  18285  znval  21492  znle  21493  uhgrspanop  29353  upgrspanop  29354  umgrspanop  29355  usgrspanop  29356  uhgrspan1lem1  29357  vtxdginducedm1lem1  29597  vtxdginducedm1fi  29602  finsumvtxdg2ssteplem4  29606  finsumvtxdg2size  29608  wlksnwwlknvbij  29965  clwwlkvbij  30172  eupthvdres  30294  eupth2lem3  30295  eupth2lemb  30296  hhssva  31317  hhsssm  31318  hhssnm  31319  hhshsslem1  31327  eulerpartlemt  34521  eulerpartgbij  34522  eulerpart  34532  fibp1  34551  actfunsnf1o  34754  subfacp1lem3  35370  subfacp1lem5  35372  dfrdg2  35981  dfrecs2  36138  finixpnum  37917  poimirlem4  37936  poimirlem9  37941  mbfresfi  37978  sdclem2  38054  diophrex  43206  rexrabdioph  43225  2rexfrabdioph  43227  3rexfrabdioph  43228  4rexfrabdioph  43229  6rexfrabdioph  43230  7rexfrabdioph  43231  rmydioph  43445  rmxdioph  43447  expdiophlem2  43453  ssnnf1octb  45627  dvnprodlem1  46378  dvnprodlem2  46379  fouriersw  46663  vonval  46972  hoidmvlelem2  47028  hoidmvlelem3  47029  iccelpart  47867  uhgrimisgrgric  48365