Theorem resex 5980

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

Syntax hints:   ∈ wcel 2109  Vcvv 3436   ↾ cres 5621

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 5235

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 3395  df-v 3438  df-in 3910  df-ss 3920  df-res 5631

This theorem is referenced by:  fprresex  8243  dfrecs3  8295  tfrlem9a  8308  domssl  8923  undom  8982  domunsncan  8994  sbthlem10  9013  mapunen  9063  dif1en  9075  ssfiALT  9088  sbthfilem  9112  php3  9123  marypha1lem  9323  infdifsn  9553  ttrclss  9616  ackbij2lem3  10134  fin1a2lem7  10300  hashf1lem2  14363  ramub2  16926  resf1st  17801  resf2nd  17802  funcres  17803  lubfval  18254  glbfval  18267  znval  21442  znle  21443  uhgrspanop  29245  upgrspanop  29246  umgrspanop  29247  usgrspanop  29248  uhgrspan1lem1  29249  vtxdginducedm1lem1  29489  vtxdginducedm1fi  29494  finsumvtxdg2ssteplem4  29498  finsumvtxdg2size  29500  wlksnwwlknvbij  29857  clwwlkvbij  30061  eupthvdres  30183  eupth2lem3  30184  eupth2lemb  30185  hhssva  31205  hhsssm  31206  hhssnm  31207  hhshsslem1  31215  eulerpartlemt  34355  eulerpartgbij  34356  eulerpart  34366  fibp1  34385  actfunsnf1o  34588  subfacp1lem3  35175  subfacp1lem5  35177  dfrdg2  35789  dfrecs2  35944  finixpnum  37605  poimirlem4  37624  poimirlem9  37629  mbfresfi  37666  sdclem2  37742  diophrex  42768  rexrabdioph  42787  2rexfrabdioph  42789  3rexfrabdioph  42790  4rexfrabdioph  42791  6rexfrabdioph  42792  7rexfrabdioph  42793  rmydioph  43007  rmxdioph  43009  expdiophlem2  43015  ssnnf1octb  45192  dvnprodlem1  45947  dvnprodlem2  45948  fouriersw  46232  vonval  46541  hoidmvlelem2  46597  hoidmvlelem3  46598  iccelpart  47437  uhgrimisgrgric  47935