Theorem resex 6026

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3453   ↾ cres 5661

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-in 3909  df-ss 3919  df-res 5671

This theorem is used by:  fprresex  8312  dfrecs3  8364  tfrlem9a  8378  domssl  9007  undom  9066  domunsncan  9078  sbthlem10  9097  mapunen  9147  dif1en  9159  ssfiALT  9171  sbthfilem  9195  php3  9206  marypha1lem  9406  infdifsn  9639  ttrclss  9702  ackbij2lem3  10245  fin1a2lem7  10411  hashf1lem2  14523  ramub2  17110  resf1st  17987  resf2nd  17988  funcres  17989  lubfval  18440  glbfval  18453  znval  21749  znle  21750  uhgrspanop  29742  upgrspanop  29743  umgrspanop  29744  usgrspanop  29745  uhgrspan1lem1  29746  vtxdginducedm1lem1  29985  vtxdginducedm1fi  29990  finsumvtxdg2ssteplem4  29994  finsumvtxdg2size  29996  wlksnwwlknvbij  30362  clwwlkvbij  30569  eupthvdres  30701  eupth2lem3  30702  eupth2lemb  30703  hhssva  31724  hhsssm  31725  hhssnm  31726  hhshsslem1  31734  eulerpartlemt  34869  eulerpartgbij  34870  eulerpart  34880  fibp1  34899  actfunsnf1o  35099  subfacp1lem3  35748  subfacp1lem5  35750  dfrdg2  36359  dfrecs2  36516  finixpnum  38346  poimirlem4  38360  poimirlem9  38365  mbfresfi  38402  sdclem2  38479  diophrex  43607  rexrabdioph  43622  2rexfrabdioph  43624  3rexfrabdioph  43625  4rexfrabdioph  43626  6rexfrabdioph  43627  7rexfrabdioph  43628  rmydioph  43842  rmxdioph  43844  expdiophlem2  43850  ssnnf1octb  46013  dvnprodlem1  46761  dvnprodlem2  46762  fouriersw  47046  vonval  47355  hoidmvlelem2  47411  hoidmvlelem3  47412  iccelpart  48320  uhgrimisgrgric  48834