Theorem resex 5985

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

Syntax hints:   ∈ wcel 2113  Vcvv 3438   ↾ cres 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5238

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3398  df-v 3440  df-in 3906  df-ss 3916  df-res 5633

This theorem is referenced by:  fprresex  8249  dfrecs3  8301  tfrlem9a  8314  domssl  8930  undom  8988  domunsncan  9000  sbthlem10  9019  mapunen  9069  dif1en  9081  ssfiALT  9093  sbthfilem  9117  php3  9128  marypha1lem  9327  infdifsn  9557  ttrclss  9620  ackbij2lem3  10141  fin1a2lem7  10307  hashf1lem2  14373  ramub2  16936  resf1st  17811  resf2nd  17812  funcres  17813  lubfval  18264  glbfval  18277  znval  21482  znle  21483  uhgrspanop  29285  upgrspanop  29286  umgrspanop  29287  usgrspanop  29288  uhgrspan1lem1  29289  vtxdginducedm1lem1  29529  vtxdginducedm1fi  29534  finsumvtxdg2ssteplem4  29538  finsumvtxdg2size  29540  wlksnwwlknvbij  29897  clwwlkvbij  30104  eupthvdres  30226  eupth2lem3  30227  eupth2lemb  30228  hhssva  31248  hhsssm  31249  hhssnm  31250  hhshsslem1  31258  eulerpartlemt  34395  eulerpartgbij  34396  eulerpart  34406  fibp1  34425  actfunsnf1o  34628  subfacp1lem3  35237  subfacp1lem5  35239  dfrdg2  35848  dfrecs2  36005  finixpnum  37655  poimirlem4  37674  poimirlem9  37679  mbfresfi  37716  sdclem2  37792  diophrex  42882  rexrabdioph  42901  2rexfrabdioph  42903  3rexfrabdioph  42904  4rexfrabdioph  42905  6rexfrabdioph  42906  7rexfrabdioph  42907  rmydioph  43121  rmxdioph  43123  expdiophlem2  43129  ssnnf1octb  45305  dvnprodlem1  46058  dvnprodlem2  46059  fouriersw  46343  vonval  46652  hoidmvlelem2  46708  hoidmvlelem3  46709  iccelpart  47547  uhgrimisgrgric  48045