Theorem resex 5987

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

Syntax hints:   ∈ wcel 2114  Vcvv 3439   ↾ cres 5625

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 5240

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 3399  df-v 3441  df-in 3907  df-ss 3917  df-res 5635

This theorem is referenced by:  fprresex  8252  dfrecs3  8304  tfrlem9a  8317  domssl  8937  undom  8995  domunsncan  9007  sbthlem10  9026  mapunen  9076  dif1en  9088  ssfiALT  9100  sbthfilem  9124  php3  9135  marypha1lem  9338  infdifsn  9568  ttrclss  9631  ackbij2lem3  10152  fin1a2lem7  10318  hashf1lem2  14381  ramub2  16944  resf1st  17820  resf2nd  17821  funcres  17822  lubfval  18273  glbfval  18286  znval  21492  znle  21493  uhgrspanop  29350  upgrspanop  29351  umgrspanop  29352  usgrspanop  29353  uhgrspan1lem1  29354  vtxdginducedm1lem1  29594  vtxdginducedm1fi  29599  finsumvtxdg2ssteplem4  29603  finsumvtxdg2size  29605  wlksnwwlknvbij  29962  clwwlkvbij  30169  eupthvdres  30291  eupth2lem3  30292  eupth2lemb  30293  hhssva  31313  hhsssm  31314  hhssnm  31315  hhshsslem1  31323  eulerpartlemt  34507  eulerpartgbij  34508  eulerpart  34518  fibp1  34537  actfunsnf1o  34740  subfacp1lem3  35355  subfacp1lem5  35357  dfrdg2  35966  dfrecs2  36123  finixpnum  37775  poimirlem4  37794  poimirlem9  37799  mbfresfi  37836  sdclem2  37912  diophrex  43054  rexrabdioph  43073  2rexfrabdioph  43075  3rexfrabdioph  43076  4rexfrabdioph  43077  6rexfrabdioph  43078  7rexfrabdioph  43079  rmydioph  43293  rmxdioph  43295  expdiophlem2  43301  ssnnf1octb  45475  dvnprodlem1  46227  dvnprodlem2  46228  fouriersw  46512  vonval  46821  hoidmvlelem2  46877  hoidmvlelem3  46878  iccelpart  47716  uhgrimisgrgric  48214