Theorem resex 5983

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

Syntax hints:   ∈ wcel 2114  Vcvv 3427   ↾ cres 5622

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 2707  ax-sep 5220

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 2714  df-cleq 2727  df-clel 2810  df-rab 3388  df-v 3429  df-in 3892  df-ss 3902  df-res 5632

This theorem is referenced by:  fprresex  8249  dfrecs3  8301  tfrlem9a  8314  domssl  8934  undom  8992  domunsncan  9004  sbthlem10  9023  mapunen  9073  dif1en  9085  ssfiALT  9097  sbthfilem  9121  php3  9132  marypha1lem  9335  infdifsn  9567  ttrclss  9630  ackbij2lem3  10151  fin1a2lem7  10317  hashf1lem2  14407  ramub2  16974  resf1st  17850  resf2nd  17851  funcres  17852  lubfval  18303  glbfval  18316  znval  21504  znle  21505  uhgrspanop  29353  upgrspanop  29354  umgrspanop  29355  usgrspanop  29356  uhgrspan1lem1  29357  vtxdginducedm1lem1  29596  vtxdginducedm1fi  29601  finsumvtxdg2ssteplem4  29605  finsumvtxdg2size  29607  wlksnwwlknvbij  29964  clwwlkvbij  30171  eupthvdres  30293  eupth2lem3  30294  eupth2lemb  30295  hhssva  31316  hhsssm  31317  hhssnm  31318  hhshsslem1  31326  eulerpartlemt  34503  eulerpartgbij  34504  eulerpart  34514  fibp1  34533  actfunsnf1o  34736  subfacp1lem3  35352  subfacp1lem5  35354  dfrdg2  35963  dfrecs2  36120  finixpnum  37914  poimirlem4  37933  poimirlem9  37938  mbfresfi  37975  sdclem2  38051  diophrex  43195  rexrabdioph  43210  2rexfrabdioph  43212  3rexfrabdioph  43213  4rexfrabdioph  43214  6rexfrabdioph  43215  7rexfrabdioph  43216  rmydioph  43430  rmxdioph  43432  expdiophlem2  43438  ssnnf1octb  45612  dvnprodlem1  46362  dvnprodlem2  46363  fouriersw  46647  vonval  46956  hoidmvlelem2  47012  hoidmvlelem3  47013  iccelpart  47881  uhgrimisgrgric  48395