Theorem resex 5989

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

Syntax hints:   ∈ wcel 2114  Vcvv 3441   ↾ cres 5627

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 5242

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 3401  df-v 3443  df-in 3909  df-ss 3919  df-res 5637

This theorem is referenced by:  fprresex  8255  dfrecs3  8307  tfrlem9a  8320  domssl  8940  undom  8998  domunsncan  9010  sbthlem10  9029  mapunen  9079  dif1en  9091  ssfiALT  9103  sbthfilem  9127  php3  9138  marypha1lem  9341  infdifsn  9571  ttrclss  9634  ackbij2lem3  10155  fin1a2lem7  10321  hashf1lem2  14384  ramub2  16947  resf1st  17823  resf2nd  17824  funcres  17825  lubfval  18276  glbfval  18289  znval  21495  znle  21496  uhgrspanop  29374  upgrspanop  29375  umgrspanop  29376  usgrspanop  29377  uhgrspan1lem1  29378  vtxdginducedm1lem1  29618  vtxdginducedm1fi  29623  finsumvtxdg2ssteplem4  29627  finsumvtxdg2size  29629  wlksnwwlknvbij  29986  clwwlkvbij  30193  eupthvdres  30315  eupth2lem3  30316  eupth2lemb  30317  hhssva  31337  hhsssm  31338  hhssnm  31339  hhshsslem1  31347  eulerpartlemt  34541  eulerpartgbij  34542  eulerpart  34552  fibp1  34571  actfunsnf1o  34774  subfacp1lem3  35389  subfacp1lem5  35391  dfrdg2  36000  dfrecs2  36157  finixpnum  37819  poimirlem4  37838  poimirlem9  37843  mbfresfi  37880  sdclem2  37956  diophrex  43095  rexrabdioph  43114  2rexfrabdioph  43116  3rexfrabdioph  43117  4rexfrabdioph  43118  6rexfrabdioph  43119  7rexfrabdioph  43120  rmydioph  43334  rmxdioph  43336  expdiophlem2  43342  ssnnf1octb  45516  dvnprodlem1  46267  dvnprodlem2  46268  fouriersw  46552  vonval  46861  hoidmvlelem2  46917  hoidmvlelem3  46918  iccelpart  47756  uhgrimisgrgric  48254