Theorem resex 6017

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

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450   ↾ cres 5652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-in 4091  df-res 5662

This theorem is used by:  fprresex  8328  dfrecs3  8380  tfrlem9a  8394  domssl  9025  undom  9084  domunsncan  9096  sbthlem10  9115  mapunen  9165  dif1en  9177  ssfiALT  9189  sbthfilem  9213  php3  9224  marypha1lem  9425  infdifsn  9658  ttrclss  9721  ackbij2lem3  10318  fin1a2lem7  10484  hashf1lem2  14601  ramub2  17192  resf1st  18069  resf2nd  18070  funcres  18071  lubfval  18522  glbfval  18535  znval  21841  znle  21842  uhgrspanop  29877  upgrspanop  29878  umgrspanop  29879  usgrspanop  29880  uhgrspan1lem1  29881  vtxdginducedm1lem1  30120  vtxdginducedm1fi  30125  finsumvtxdg2ssteplem4  30129  finsumvtxdg2size  30131  wlksnwwlknvbij  30497  clwwlkvbij  30704  eupthvdres  30836  eupth2lem3  30837  eupth2lemb  30838  hhssva  31859  hhsssm  31860  hhssnm  31861  hhshsslem1  31869  eulerpartlemt  35003  eulerpartgbij  35004  eulerpart  35014  fibp1  35033  actfunsnf1o  35233  subfacp1lem3  35947  subfacp1lem5  35949  dfrdg2  36557  dfrecs2  36714  finixpnum  38529  poimirlem4  38543  poimirlem9  38548  mbfresfi  38585  sdclem2  38677  diophrex  43786  rexrabdioph  43801  2rexfrabdioph  43803  3rexfrabdioph  43804  4rexfrabdioph  43805  6rexfrabdioph  43806  7rexfrabdioph  43807  rmydioph  44021  rmxdioph  44023  expdiophlem2  44029  ssnnf1octb  46209  dvnprodlem1  46956  dvnprodlem2  46957  fouriersw  47241  vonval  47550  hoidmvlelem2  47606  hoidmvlelem3  47607  iccelpart  48515  uhgrimisgrgric  49029