Theorem resex 6000

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

Syntax hints:   ∈ wcel 2109  Vcvv 3447   ↾ cres 5640

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-in 3921  df-ss 3931  df-res 5650

This theorem is referenced by:  fprresex  8289  dfrecs3  8341  tfrlem9a  8354  domssl  8969  undom  9029  domunsncan  9041  sbthlem10  9060  mapunen  9110  dif1en  9124  dif1enOLD  9126  ssfiALT  9138  sbthfilem  9162  php3  9173  marypha1lem  9384  infdifsn  9610  ttrclss  9673  ackbij2lem3  10193  fin1a2lem7  10359  hashf1lem2  14421  ramub2  16985  resf1st  17856  resf2nd  17857  funcres  17858  lubfval  18309  glbfval  18322  znval  21445  znle  21446  uhgrspanop  29223  upgrspanop  29224  umgrspanop  29225  usgrspanop  29226  uhgrspan1lem1  29227  vtxdginducedm1lem1  29467  vtxdginducedm1fi  29472  finsumvtxdg2ssteplem4  29476  finsumvtxdg2size  29478  wlksnwwlknvbij  29838  clwwlkvbij  30042  eupthvdres  30164  eupth2lem3  30165  eupth2lemb  30166  hhssva  31186  hhsssm  31187  hhssnm  31188  hhshsslem1  31196  eulerpartlemt  34362  eulerpartgbij  34363  eulerpart  34373  fibp1  34392  actfunsnf1o  34595  subfacp1lem3  35169  subfacp1lem5  35171  dfrdg2  35783  dfrecs2  35938  finixpnum  37599  poimirlem4  37618  poimirlem9  37623  mbfresfi  37660  sdclem2  37736  diophrex  42763  rexrabdioph  42782  2rexfrabdioph  42784  3rexfrabdioph  42785  4rexfrabdioph  42786  6rexfrabdioph  42787  7rexfrabdioph  42788  rmydioph  43003  rmxdioph  43005  expdiophlem2  43011  ssnnf1octb  45188  dvnprodlem1  45944  dvnprodlem2  45945  fouriersw  46229  vonval  46538  hoidmvlelem2  46594  hoidmvlelem3  46595  iccelpart  47434  uhgrimisgrgric  47931