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 2141  Vcvv 3453   ↾ cres 5663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5256

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3415  df-v 3455  df-in 3911  df-ss 3921  df-res 5673

This theorem is referenced by:  fprresex  8306  dfrecs3  8358  tfrlem9a  8372  domssl  8994  undom  9052  domunsncan  9064  sbthlem10  9083  mapunen  9133  dif1en  9145  ssfiALT  9157  sbthfilem  9181  php3  9192  marypha1lem  9392  infdifsn  9625  ttrclss  9688  ackbij2lem3  10222  fin1a2lem7  10389  hashf1lem2  14492  ramub2  17073  resf1st  17950  resf2nd  17951  funcres  17952  lubfval  18403  glbfval  18416  znval  21664  znle  21665  uhgrspanop  29612  upgrspanop  29613  umgrspanop  29614  usgrspanop  29615  uhgrspan1lem1  29616  vtxdginducedm1lem1  29855  vtxdginducedm1fi  29860  finsumvtxdg2ssteplem4  29864  finsumvtxdg2size  29866  wlksnwwlknvbij  30223  clwwlkvbij  30430  eupthvdres  30552  eupth2lem3  30553  eupth2lemb  30554  hhssva  31575  hhsssm  31576  hhssnm  31577  hhshsslem1  31585  eulerpartlemt  34727  eulerpartgbij  34728  eulerpart  34738  fibp1  34757  actfunsnf1o  34957  subfacp1lem3  35628  subfacp1lem5  35630  dfrdg2  36239  dfrecs2  36396  finixpnum  38200  poimirlem4  38219  poimirlem9  38224  mbfresfi  38261  sdclem2  38337  diophrex  43454  rexrabdioph  43469  2rexfrabdioph  43471  3rexfrabdioph  43472  4rexfrabdioph  43473  6rexfrabdioph  43474  7rexfrabdioph  43475  rmydioph  43689  rmxdioph  43691  expdiophlem2  43697  ssnnf1octb  45860  dvnprodlem1  46608  dvnprodlem2  46609  fouriersw  46893  vonval  47202  hoidmvlelem2  47258  hoidmvlelem3  47259  iccelpart  48127  uhgrimisgrgric  48641