Theorem resex 5785

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

Syntax hints:   ∈ wcel 2081  Vcvv 3437   ↾ cres 5450

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769  ax-sep 5099

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-v 3439  df-in 3870  df-ss 3878  df-res 5460

This theorem is referenced by:  wfrlem17  7828  tfrlem9a  7879  domunsncan  8469  sbthlem10  8488  mapunen  8538  php3  8555  ssfi  8589  marypha1lem  8748  infdifsn  8971  ackbij2lem3  9514  fin1a2lem7  9679  hashf1lem2  13667  ramub2  16184  resf1st  16998  resf2nd  16999  funcres  17000  lubfval  17422  glbfval  17435  znval  20369  znle  20370  uhgrspanop  26766  upgrspanop  26767  umgrspanop  26768  usgrspanop  26769  uhgrspan1lem1  26770  vtxdginducedm1lem1  27009  vtxdginducedm1fi  27014  finsumvtxdg2ssteplem4  27018  finsumvtxdg2size  27020  wlksnwwlknvbij  27379  clwwlkvbij  27584  eupthvdres  27707  eupth2lem3  27708  eupth2lemb  27709  hhssva  28730  hhsssm  28731  hhssnm  28732  hhshsslem1  28740  eulerpartlemt  31251  eulerpartgbij  31252  eulerpart  31262  fibp1  31281  actfunsnf1o  31497  subfacp1lem3  32044  subfacp1lem5  32046  dfrdg2  32656  dfrecs2  33027  finixpnum  34434  poimirlem4  34453  poimirlem9  34458  mbfresfi  34495  sdclem2  34575  diophrex  38883  rexrabdioph  38902  2rexfrabdioph  38904  3rexfrabdioph  38905  4rexfrabdioph  38906  6rexfrabdioph  38907  7rexfrabdioph  38908  rmydioph  39122  rmxdioph  39124  expdiophlem2  39130  ssnnf1octb  41022  dvnprodlem1  41799  dvnprodlem2  41800  fouriersw  42085  vonval  42391  hoidmvlelem2  42447  hoidmvlelem3  42448  iccelpart  43102