Theorem resex 5942

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

Syntax hints:   ∈ wcel 2107  Vcvv 3433   ↾ cres 5592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-sep 5224

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-in 3895  df-ss 3905  df-res 5602

This theorem is referenced by:  fprresex  8135  dfwrecsOLD  8138  wfrlem17OLD  8165  dfrecs3  8212  tfrlem9a  8226  undom  8855  domunsncan  8868  sbthlem10  8888  mapunen  8942  dif1en  8954  ssfiALT  8966  sbthfilem  8993  php3  9004  php3OLD  9016  marypha1lem  9201  infdifsn  9424  ttrclss  9487  ackbij2lem3  10006  fin1a2lem7  10171  hashf1lem2  14179  ramub2  16724  resf1st  17618  resf2nd  17619  funcres  17620  lubfval  18077  glbfval  18090  znval  20748  znle  20749  uhgrspanop  27672  upgrspanop  27673  umgrspanop  27674  usgrspanop  27675  uhgrspan1lem1  27676  vtxdginducedm1lem1  27915  vtxdginducedm1fi  27920  finsumvtxdg2ssteplem4  27924  finsumvtxdg2size  27926  wlksnwwlknvbij  28282  clwwlkvbij  28486  eupthvdres  28608  eupth2lem3  28609  eupth2lemb  28610  hhssva  29628  hhsssm  29629  hhssnm  29630  hhshsslem1  29638  eulerpartlemt  32347  eulerpartgbij  32348  eulerpart  32358  fibp1  32377  actfunsnf1o  32593  subfacp1lem3  33153  subfacp1lem5  33155  dfrdg2  33780  dfrecs2  34261  finixpnum  35771  poimirlem4  35790  poimirlem9  35795  mbfresfi  35832  sdclem2  35909  diophrex  40604  rexrabdioph  40623  2rexfrabdioph  40625  3rexfrabdioph  40626  4rexfrabdioph  40627  6rexfrabdioph  40628  7rexfrabdioph  40629  rmydioph  40843  rmxdioph  40845  expdiophlem2  40851  ssnnf1octb  42740  dvnprodlem1  43494  dvnprodlem2  43495  fouriersw  43779  vonval  44085  hoidmvlelem2  44141  hoidmvlelem3  44142  iccelpart  44896