Theorem resex 6047

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

Syntax hints:   ∈ wcel 2108  Vcvv 3480   ↾ cres 5687

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-in 3958  df-ss 3968  df-res 5697

This theorem is referenced by:  fprresex  8335  dfwrecsOLD  8338  wfrlem17OLD  8365  dfrecs3  8412  tfrlem9a  8426  domssl  9038  undom  9099  domunsncan  9112  sbthlem10  9132  mapunen  9186  dif1en  9200  dif1enOLD  9202  ssfiALT  9214  sbthfilem  9238  php3  9249  php3OLD  9261  marypha1lem  9473  infdifsn  9697  ttrclss  9760  ackbij2lem3  10280  fin1a2lem7  10446  hashf1lem2  14495  ramub2  17052  resf1st  17939  resf2nd  17940  funcres  17941  lubfval  18395  glbfval  18408  znval  21550  znle  21551  uhgrspanop  29313  upgrspanop  29314  umgrspanop  29315  usgrspanop  29316  uhgrspan1lem1  29317  vtxdginducedm1lem1  29557  vtxdginducedm1fi  29562  finsumvtxdg2ssteplem4  29566  finsumvtxdg2size  29568  wlksnwwlknvbij  29928  clwwlkvbij  30132  eupthvdres  30254  eupth2lem3  30255  eupth2lemb  30256  hhssva  31276  hhsssm  31277  hhssnm  31278  hhshsslem1  31286  eulerpartlemt  34373  eulerpartgbij  34374  eulerpart  34384  fibp1  34403  actfunsnf1o  34619  subfacp1lem3  35187  subfacp1lem5  35189  dfrdg2  35796  dfrecs2  35951  finixpnum  37612  poimirlem4  37631  poimirlem9  37636  mbfresfi  37673  sdclem2  37749  diophrex  42786  rexrabdioph  42805  2rexfrabdioph  42807  3rexfrabdioph  42808  4rexfrabdioph  42809  6rexfrabdioph  42810  7rexfrabdioph  42811  rmydioph  43026  rmxdioph  43028  expdiophlem2  43034  ssnnf1octb  45199  dvnprodlem1  45961  dvnprodlem2  45962  fouriersw  46246  vonval  46555  hoidmvlelem2  46611  hoidmvlelem3  46612  iccelpart  47420  uhgrimisgrgric  47899