Theorem resex 6017

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

Syntax hints:   ∈ wcel 2144  Vcvv 3456   ↾ cres 5651

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-sep 5248

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1101  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-in 3913  df-ss 3923  df-res 5661

This theorem is referenced by:  fprresex  8293  dfrecs3  8345  tfrlem9a  8359  domssl  8981  undom  9039  domunsncan  9051  sbthlem10  9070  mapunen  9120  dif1en  9132  ssfiALT  9144  sbthfilem  9168  php3  9179  marypha1lem  9381  infdifsn  9614  ttrclss  9677  ackbij2lem3  10198  fin1a2lem7  10365  hashf1lem2  14471  ramub2  17052  resf1st  17929  resf2nd  17930  funcres  17931  lubfval  18382  glbfval  18395  znval  21589  znle  21590  uhgrspanop  29499  upgrspanop  29500  umgrspanop  29501  usgrspanop  29502  uhgrspan1lem1  29503  vtxdginducedm1lem1  29742  vtxdginducedm1fi  29747  finsumvtxdg2ssteplem4  29751  finsumvtxdg2size  29753  wlksnwwlknvbij  30110  clwwlkvbij  30317  eupthvdres  30439  eupth2lem3  30440  eupth2lemb  30441  hhssva  31462  hhsssm  31463  hhssnm  31464  hhshsslem1  31472  eulerpartlemt  34670  eulerpartgbij  34671  eulerpart  34681  fibp1  34700  actfunsnf1o  34900  subfacp1lem3  35537  subfacp1lem5  35539  dfrdg2  36148  dfrecs2  36305  finixpnum  38109  poimirlem4  38128  poimirlem9  38133  mbfresfi  38170  sdclem2  38246  diophrex  43361  rexrabdioph  43376  2rexfrabdioph  43378  3rexfrabdioph  43379  4rexfrabdioph  43380  6rexfrabdioph  43381  7rexfrabdioph  43382  rmydioph  43596  rmxdioph  43598  expdiophlem2  43604  ssnnf1octb  45777  dvnprodlem1  46525  dvnprodlem2  46526  fouriersw  46810  vonval  47119  hoidmvlelem2  47175  hoidmvlelem3  47176  iccelpart  48044  uhgrimisgrgric  48558