Theorem resex 6058

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

Syntax hints:   ∈ wcel 2108  Vcvv 3488   ↾ cres 5702

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-in 3983  df-ss 3993  df-res 5712

This theorem is referenced by:  fprresex  8351  dfwrecsOLD  8354  wfrlem17OLD  8381  dfrecs3  8428  tfrlem9a  8442  domssl  9058  undom  9125  domunsncan  9138  sbthlem10  9158  mapunen  9212  dif1en  9226  dif1enOLD  9228  ssfiALT  9241  sbthfilem  9264  php3  9275  php3OLD  9287  marypha1lem  9502  infdifsn  9726  ttrclss  9789  ackbij2lem3  10309  fin1a2lem7  10475  hashf1lem2  14505  ramub2  17061  resf1st  17958  resf2nd  17959  funcres  17960  lubfval  18420  glbfval  18433  znval  21573  znle  21574  uhgrspanop  29331  upgrspanop  29332  umgrspanop  29333  usgrspanop  29334  uhgrspan1lem1  29335  vtxdginducedm1lem1  29575  vtxdginducedm1fi  29580  finsumvtxdg2ssteplem4  29584  finsumvtxdg2size  29586  wlksnwwlknvbij  29941  clwwlkvbij  30145  eupthvdres  30267  eupth2lem3  30268  eupth2lemb  30269  hhssva  31289  hhsssm  31290  hhssnm  31291  hhshsslem1  31299  eulerpartlemt  34336  eulerpartgbij  34337  eulerpart  34347  fibp1  34366  actfunsnf1o  34581  subfacp1lem3  35150  subfacp1lem5  35152  dfrdg2  35759  dfrecs2  35914  finixpnum  37565  poimirlem4  37584  poimirlem9  37589  mbfresfi  37626  sdclem2  37702  diophrex  42731  rexrabdioph  42750  2rexfrabdioph  42752  3rexfrabdioph  42753  4rexfrabdioph  42754  6rexfrabdioph  42755  7rexfrabdioph  42756  rmydioph  42971  rmxdioph  42973  expdiophlem2  42979  ssnnf1octb  45101  dvnprodlem1  45867  dvnprodlem2  45868  fouriersw  46152  vonval  46461  hoidmvlelem2  46517  hoidmvlelem3  46518  iccelpart  47307  uhgrimisgrgric  47783