Theorem resex 5977

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

Syntax hints:   ∈ wcel 2111  Vcvv 3436   ↾ cres 5616

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 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-in 3904  df-ss 3914  df-res 5626

This theorem is referenced by:  fprresex  8240  dfrecs3  8292  tfrlem9a  8305  domssl  8920  undom  8978  domunsncan  8990  sbthlem10  9009  mapunen  9059  dif1en  9071  ssfiALT  9083  sbthfilem  9107  php3  9118  marypha1lem  9317  infdifsn  9547  ttrclss  9610  ackbij2lem3  10131  fin1a2lem7  10297  hashf1lem2  14363  ramub2  16926  resf1st  17801  resf2nd  17802  funcres  17803  lubfval  18254  glbfval  18267  znval  21472  znle  21473  uhgrspanop  29274  upgrspanop  29275  umgrspanop  29276  usgrspanop  29277  uhgrspan1lem1  29278  vtxdginducedm1lem1  29518  vtxdginducedm1fi  29523  finsumvtxdg2ssteplem4  29527  finsumvtxdg2size  29529  wlksnwwlknvbij  29886  clwwlkvbij  30093  eupthvdres  30215  eupth2lem3  30216  eupth2lemb  30217  hhssva  31237  hhsssm  31238  hhssnm  31239  hhshsslem1  31247  eulerpartlemt  34384  eulerpartgbij  34385  eulerpart  34395  fibp1  34414  actfunsnf1o  34617  subfacp1lem3  35226  subfacp1lem5  35228  dfrdg2  35837  dfrecs2  35994  finixpnum  37644  poimirlem4  37663  poimirlem9  37668  mbfresfi  37705  sdclem2  37781  diophrex  42867  rexrabdioph  42886  2rexfrabdioph  42888  3rexfrabdioph  42889  4rexfrabdioph  42890  6rexfrabdioph  42891  7rexfrabdioph  42892  rmydioph  43106  rmxdioph  43108  expdiophlem2  43114  ssnnf1octb  45290  dvnprodlem1  46043  dvnprodlem2  46044  fouriersw  46328  vonval  46637  hoidmvlelem2  46693  hoidmvlelem3  46694  iccelpart  47532  uhgrimisgrgric  48030