Theorem resex 5989

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

Syntax hints:   ∈ wcel 2109  Vcvv 3444   ↾ cres 5633

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 5246

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 3403  df-v 3446  df-in 3918  df-ss 3928  df-res 5643

This theorem is referenced by:  fprresex  8266  dfrecs3  8318  tfrlem9a  8331  domssl  8946  undom  9006  domunsncan  9018  sbthlem10  9037  mapunen  9087  dif1en  9101  dif1enOLD  9103  ssfiALT  9115  sbthfilem  9139  php3  9150  marypha1lem  9360  infdifsn  9588  ttrclss  9651  ackbij2lem3  10171  fin1a2lem7  10337  hashf1lem2  14399  ramub2  16962  resf1st  17837  resf2nd  17838  funcres  17839  lubfval  18290  glbfval  18303  znval  21478  znle  21479  uhgrspanop  29277  upgrspanop  29278  umgrspanop  29279  usgrspanop  29280  uhgrspan1lem1  29281  vtxdginducedm1lem1  29521  vtxdginducedm1fi  29526  finsumvtxdg2ssteplem4  29530  finsumvtxdg2size  29532  wlksnwwlknvbij  29889  clwwlkvbij  30093  eupthvdres  30215  eupth2lem3  30216  eupth2lemb  30217  hhssva  31237  hhsssm  31238  hhssnm  31239  hhshsslem1  31247  eulerpartlemt  34356  eulerpartgbij  34357  eulerpart  34367  fibp1  34386  actfunsnf1o  34589  subfacp1lem3  35163  subfacp1lem5  35165  dfrdg2  35777  dfrecs2  35932  finixpnum  37593  poimirlem4  37612  poimirlem9  37617  mbfresfi  37654  sdclem2  37730  diophrex  42757  rexrabdioph  42776  2rexfrabdioph  42778  3rexfrabdioph  42779  4rexfrabdioph  42780  6rexfrabdioph  42781  7rexfrabdioph  42782  rmydioph  42997  rmxdioph  42999  expdiophlem2  43005  ssnnf1octb  45182  dvnprodlem1  45938  dvnprodlem2  45939  fouriersw  46223  vonval  46532  hoidmvlelem2  46588  hoidmvlelem3  46589  iccelpart  47428  uhgrimisgrgric  47925