Theorem resex 6049

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

Syntax hints:   ∈ wcel 2106  Vcvv 3478   ↾ cres 5691

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-in 3970  df-ss 3980  df-res 5701

This theorem is referenced by:  fprresex  8334  dfwrecsOLD  8337  wfrlem17OLD  8364  dfrecs3  8411  tfrlem9a  8425  domssl  9037  undom  9098  domunsncan  9111  sbthlem10  9131  mapunen  9185  dif1en  9199  dif1enOLD  9201  ssfiALT  9213  sbthfilem  9236  php3  9247  php3OLD  9259  marypha1lem  9471  infdifsn  9695  ttrclss  9758  ackbij2lem3  10278  fin1a2lem7  10444  hashf1lem2  14492  ramub2  17048  resf1st  17945  resf2nd  17946  funcres  17947  lubfval  18408  glbfval  18421  znval  21568  znle  21569  uhgrspanop  29328  upgrspanop  29329  umgrspanop  29330  usgrspanop  29331  uhgrspan1lem1  29332  vtxdginducedm1lem1  29572  vtxdginducedm1fi  29577  finsumvtxdg2ssteplem4  29581  finsumvtxdg2size  29583  wlksnwwlknvbij  29938  clwwlkvbij  30142  eupthvdres  30264  eupth2lem3  30265  eupth2lemb  30266  hhssva  31286  hhsssm  31287  hhssnm  31288  hhshsslem1  31296  eulerpartlemt  34353  eulerpartgbij  34354  eulerpart  34364  fibp1  34383  actfunsnf1o  34598  subfacp1lem3  35167  subfacp1lem5  35169  dfrdg2  35777  dfrecs2  35932  finixpnum  37592  poimirlem4  37611  poimirlem9  37616  mbfresfi  37653  sdclem2  37729  diophrex  42763  rexrabdioph  42782  2rexfrabdioph  42784  3rexfrabdioph  42785  4rexfrabdioph  42786  6rexfrabdioph  42787  7rexfrabdioph  42788  rmydioph  43003  rmxdioph  43005  expdiophlem2  43011  ssnnf1octb  45137  dvnprodlem1  45902  dvnprodlem2  45903  fouriersw  46187  vonval  46496  hoidmvlelem2  46552  hoidmvlelem3  46553  iccelpart  47358  uhgrimisgrgric  47837