Theorem resex 5987

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

Syntax hints:   ∈ wcel 2121  Vcvv 3433   ↾ cres 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5220

This theorem depends on definitions:  df-bi 209  df-an 398  df-3an 1095  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-in 3891  df-ss 3901  df-res 5632

This theorem is referenced by:  fprresex  8253  dfrecs3  8305  tfrlem9a  8319  domssl  8939  undom  8997  domunsncan  9009  sbthlem10  9028  mapunen  9078  dif1en  9090  ssfiALT  9102  sbthfilem  9126  php3  9137  marypha1lem  9340  infdifsn  9573  ttrclss  9636  ackbij2lem3  10157  fin1a2lem7  10324  hashf1lem2  14413  ramub2  16980  resf1st  17856  resf2nd  17857  funcres  17858  lubfval  18309  glbfval  18322  znval  21513  znle  21514  uhgrspanop  29385  upgrspanop  29386  umgrspanop  29387  usgrspanop  29388  uhgrspan1lem1  29389  vtxdginducedm1lem1  29628  vtxdginducedm1fi  29633  finsumvtxdg2ssteplem4  29637  finsumvtxdg2size  29639  wlksnwwlknvbij  29996  clwwlkvbij  30203  eupthvdres  30325  eupth2lem3  30326  eupth2lemb  30327  hhssva  31348  hhsssm  31349  hhssnm  31350  hhshsslem1  31358  eulerpartlemt  34565  eulerpartgbij  34566  eulerpart  34576  fibp1  34595  actfunsnf1o  34798  subfacp1lem3  35423  subfacp1lem5  35425  dfrdg2  36034  dfrecs2  36191  finixpnum  37985  poimirlem4  38004  poimirlem9  38009  mbfresfi  38046  sdclem2  38122  diophrex  43237  rexrabdioph  43252  2rexfrabdioph  43254  3rexfrabdioph  43255  4rexfrabdioph  43256  6rexfrabdioph  43257  7rexfrabdioph  43258  rmydioph  43472  rmxdioph  43474  expdiophlem2  43480  ssnnf1octb  45653  dvnprodlem1  46401  dvnprodlem2  46402  fouriersw  46686  vonval  46995  hoidmvlelem2  47051  hoidmvlelem3  47052  iccelpart  47920  uhgrimisgrgric  48434