Theorem resex 6029

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

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454   ↾ cres 5657

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-in 4094  df-res 5667

This theorem is used by:  fprresex  8353  dfrecs3  8405  tfrlem9a  8419  domssl  9050  undom  9109  domunsncan  9121  sbthlem10  9140  mapunen  9190  dif1en  9202  ssfiALT  9214  sbthfilem  9238  php3  9249  marypha1lem  9449  infdifsn  9682  ttrclss  9745  ackbij2lem3  10342  fin1a2lem7  10508  hashf1lem2  14625  ramub2  17218  resf1st  18095  resf2nd  18096  funcres  18097  lubfval  18548  glbfval  18561  znval  21868  znle  21869  uhgrspanop  29904  upgrspanop  29905  umgrspanop  29906  usgrspanop  29907  uhgrspan1lem1  29908  vtxdginducedm1lem1  30147  vtxdginducedm1fi  30152  finsumvtxdg2ssteplem4  30156  finsumvtxdg2size  30158  wlksnwwlknvbij  30524  clwwlkvbij  30731  eupthvdres  30863  eupth2lem3  30864  eupth2lemb  30865  hhssva  31886  hhsssm  31887  hhssnm  31888  hhshsslem1  31896  eulerpartlemt  35070  eulerpartgbij  35071  eulerpart  35081  fibp1  35100  actfunsnf1o  35300  subfacp1lem3  36113  subfacp1lem5  36115  dfrdg2  36734  dfrecs2  36891  finixpnum  38719  poimirlem4  38733  poimirlem9  38738  mbfresfi  38775  sdclem2  38867  diophrex  43977  rexrabdioph  43992  2rexfrabdioph  43994  3rexfrabdioph  43995  4rexfrabdioph  43996  6rexfrabdioph  43997  7rexfrabdioph  43998  rmydioph  44212  rmxdioph  44214  expdiophlem2  44220  ssnnf1octb  46412  dvnprodlem1  47159  dvnprodlem2  47160  fouriersw  47444  vonval  47753  hoidmvlelem2  47809  hoidmvlelem3  47810  iccelpart  48718  uhgrimisgrgric  49232