Theorem resex 5899

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

Syntax hints:   ∈ wcel 2114  Vcvv 3494   ↾ cres 5557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-in 3943  df-ss 3952  df-res 5567

This theorem is referenced by:  wfrlem17  7971  tfrlem9a  8022  domunsncan  8617  sbthlem10  8636  mapunen  8686  php3  8703  ssfi  8738  marypha1lem  8897  infdifsn  9120  ackbij2lem3  9663  fin1a2lem7  9828  hashf1lem2  13815  ramub2  16350  resf1st  17164  resf2nd  17165  funcres  17166  lubfval  17588  glbfval  17601  znval  20682  znle  20683  uhgrspanop  27078  upgrspanop  27079  umgrspanop  27080  usgrspanop  27081  uhgrspan1lem1  27082  vtxdginducedm1lem1  27321  vtxdginducedm1fi  27326  finsumvtxdg2ssteplem4  27330  finsumvtxdg2size  27332  wlksnwwlknvbij  27687  clwwlkvbij  27892  eupthvdres  28014  eupth2lem3  28015  eupth2lemb  28016  hhssva  29034  hhsssm  29035  hhssnm  29036  hhshsslem1  29044  eulerpartlemt  31629  eulerpartgbij  31630  eulerpart  31640  fibp1  31659  actfunsnf1o  31875  subfacp1lem3  32429  subfacp1lem5  32431  dfrdg2  33040  dfrecs2  33411  finixpnum  34892  poimirlem4  34911  poimirlem9  34916  mbfresfi  34953  sdclem2  35032  diophrex  39392  rexrabdioph  39411  2rexfrabdioph  39413  3rexfrabdioph  39414  4rexfrabdioph  39415  6rexfrabdioph  39416  7rexfrabdioph  39417  rmydioph  39631  rmxdioph  39633  expdiophlem2  39639  ssnnf1octb  41476  dvnprodlem1  42251  dvnprodlem2  42252  fouriersw  42536  vonval  42842  hoidmvlelem2  42898  hoidmvlelem3  42899  iccelpart  43613