Theorem resex 5992

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

Syntax hints:   ∈ wcel 2114  Vcvv 3430   ↾ cres 5630

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 5232

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 5640

This theorem is referenced by:  fprresex  8257  dfrecs3  8309  tfrlem9a  8322  domssl  8942  undom  9000  domunsncan  9012  sbthlem10  9031  mapunen  9081  dif1en  9093  ssfiALT  9105  sbthfilem  9129  php3  9140  marypha1lem  9343  infdifsn  9575  ttrclss  9638  ackbij2lem3  10159  fin1a2lem7  10325  hashf1lem2  14415  ramub2  16982  resf1st  17858  resf2nd  17859  funcres  17860  lubfval  18311  glbfval  18324  znval  21512  znle  21513  uhgrspanop  29362  upgrspanop  29363  umgrspanop  29364  usgrspanop  29365  uhgrspan1lem1  29366  vtxdginducedm1lem1  29605  vtxdginducedm1fi  29610  finsumvtxdg2ssteplem4  29614  finsumvtxdg2size  29616  wlksnwwlknvbij  29973  clwwlkvbij  30180  eupthvdres  30302  eupth2lem3  30303  eupth2lemb  30304  hhssva  31325  hhsssm  31326  hhssnm  31327  hhshsslem1  31335  eulerpartlemt  34512  eulerpartgbij  34513  eulerpart  34523  fibp1  34542  actfunsnf1o  34745  subfacp1lem3  35361  subfacp1lem5  35363  dfrdg2  35972  dfrecs2  36129  finixpnum  37923  poimirlem4  37942  poimirlem9  37947  mbfresfi  37984  sdclem2  38060  diophrex  43204  rexrabdioph  43219  2rexfrabdioph  43221  3rexfrabdioph  43222  4rexfrabdioph  43223  6rexfrabdioph  43224  7rexfrabdioph  43225  rmydioph  43439  rmxdioph  43441  expdiophlem2  43447  ssnnf1octb  45621  dvnprodlem1  46371  dvnprodlem2  46372  fouriersw  46656  vonval  46965  hoidmvlelem2  47021  hoidmvlelem3  47022  iccelpart  47884  uhgrimisgrgric  48398