Theorem resex 6028

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

Syntax hints:   ∈ wcel 2104  Vcvv 3472   ↾ cres 5677

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5298

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-in 3954  df-ss 3964  df-res 5687

This theorem is referenced by:  fprresex  8297  dfwrecsOLD  8300  wfrlem17OLD  8327  dfrecs3  8374  tfrlem9a  8388  domssl  8996  undom  9061  domunsncan  9074  sbthlem10  9094  mapunen  9148  dif1en  9162  dif1enOLD  9164  ssfiALT  9176  sbthfilem  9203  php3  9214  php3OLD  9226  marypha1lem  9430  infdifsn  9654  ttrclss  9717  ackbij2lem3  10238  fin1a2lem7  10403  hashf1lem2  14421  ramub2  16951  resf1st  17848  resf2nd  17849  funcres  17850  lubfval  18307  glbfval  18320  znval  21306  znle  21307  uhgrspanop  28820  upgrspanop  28821  umgrspanop  28822  usgrspanop  28823  uhgrspan1lem1  28824  vtxdginducedm1lem1  29063  vtxdginducedm1fi  29068  finsumvtxdg2ssteplem4  29072  finsumvtxdg2size  29074  wlksnwwlknvbij  29429  clwwlkvbij  29633  eupthvdres  29755  eupth2lem3  29756  eupth2lemb  29757  hhssva  30777  hhsssm  30778  hhssnm  30779  hhshsslem1  30787  eulerpartlemt  33668  eulerpartgbij  33669  eulerpart  33679  fibp1  33698  actfunsnf1o  33914  subfacp1lem3  34471  subfacp1lem5  34473  dfrdg2  35071  dfrecs2  35226  finixpnum  36776  poimirlem4  36795  poimirlem9  36800  mbfresfi  36837  sdclem2  36913  diophrex  41815  rexrabdioph  41834  2rexfrabdioph  41836  3rexfrabdioph  41837  4rexfrabdioph  41838  6rexfrabdioph  41839  7rexfrabdioph  41840  rmydioph  42055  rmxdioph  42057  expdiophlem2  42063  ssnnf1octb  44191  dvnprodlem1  44960  dvnprodlem2  44961  fouriersw  45245  vonval  45554  hoidmvlelem2  45610  hoidmvlelem3  45611  iccelpart  46399