Theorem resex 5958

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

Syntax hints:   ∈ wcel 2105  Vcvv 3441   ↾ cres 5609

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708  ax-sep 5238

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3405  df-v 3443  df-in 3904  df-ss 3914  df-res 5619

This theorem is referenced by:  fprresex  8173  dfwrecsOLD  8176  wfrlem17OLD  8203  dfrecs3  8250  tfrlem9a  8264  domssl  8836  undom  8901  domunsncan  8914  sbthlem10  8934  mapunen  8988  dif1en  9002  dif1enOLD  9004  ssfiALT  9016  sbthfilem  9043  php3  9054  php3OLD  9066  marypha1lem  9262  infdifsn  9486  ttrclss  9549  ackbij2lem3  10070  fin1a2lem7  10235  hashf1lem2  14242  ramub2  16785  resf1st  17679  resf2nd  17680  funcres  17681  lubfval  18138  glbfval  18151  znval  20811  znle  20812  uhgrspanop  27772  upgrspanop  27773  umgrspanop  27774  usgrspanop  27775  uhgrspan1lem1  27776  vtxdginducedm1lem1  28015  vtxdginducedm1fi  28020  finsumvtxdg2ssteplem4  28024  finsumvtxdg2size  28026  wlksnwwlknvbij  28382  clwwlkvbij  28586  eupthvdres  28708  eupth2lem3  28709  eupth2lemb  28710  hhssva  29728  hhsssm  29729  hhssnm  29730  hhshsslem1  29738  eulerpartlemt  32444  eulerpartgbij  32445  eulerpart  32455  fibp1  32474  actfunsnf1o  32690  subfacp1lem3  33249  subfacp1lem5  33251  dfrdg2  33870  dfrecs2  34310  finixpnum  35818  poimirlem4  35837  poimirlem9  35842  mbfresfi  35879  sdclem2  35956  diophrex  40800  rexrabdioph  40819  2rexfrabdioph  40821  3rexfrabdioph  40822  4rexfrabdioph  40823  6rexfrabdioph  40824  7rexfrabdioph  40825  rmydioph  41040  rmxdioph  41042  expdiophlem2  41048  ssnnf1octb  42961  dvnprodlem1  43724  dvnprodlem2  43725  fouriersw  44009  vonval  44316  hoidmvlelem2  44372  hoidmvlelem3  44373  iccelpart  45137