Theorem resex 5990

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

Syntax hints:   ∈ wcel 2109  Vcvv 3444   ↾ cres 5633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-in 3918  df-ss 3928  df-res 5643

This theorem is referenced by:  fprresex  8267  dfrecs3  8319  tfrlem9a  8332  domssl  8947  undom  9007  domunsncan  9019  sbthlem10  9038  mapunen  9088  dif1en  9102  dif1enOLD  9104  ssfiALT  9116  sbthfilem  9140  php3  9151  marypha1lem  9361  infdifsn  9589  ttrclss  9652  ackbij2lem3  10172  fin1a2lem7  10338  hashf1lem2  14400  ramub2  16963  resf1st  17838  resf2nd  17839  funcres  17840  lubfval  18291  glbfval  18304  znval  21479  znle  21480  uhgrspanop  29278  upgrspanop  29279  umgrspanop  29280  usgrspanop  29281  uhgrspan1lem1  29282  vtxdginducedm1lem1  29522  vtxdginducedm1fi  29527  finsumvtxdg2ssteplem4  29531  finsumvtxdg2size  29533  wlksnwwlknvbij  29890  clwwlkvbij  30094  eupthvdres  30216  eupth2lem3  30217  eupth2lemb  30218  hhssva  31238  hhsssm  31239  hhssnm  31240  hhshsslem1  31248  eulerpartlemt  34357  eulerpartgbij  34358  eulerpart  34368  fibp1  34387  actfunsnf1o  34590  subfacp1lem3  35164  subfacp1lem5  35166  dfrdg2  35778  dfrecs2  35933  finixpnum  37594  poimirlem4  37613  poimirlem9  37618  mbfresfi  37655  sdclem2  37731  diophrex  42758  rexrabdioph  42777  2rexfrabdioph  42779  3rexfrabdioph  42780  4rexfrabdioph  42781  6rexfrabdioph  42782  7rexfrabdioph  42783  rmydioph  42998  rmxdioph  43000  expdiophlem2  43006  ssnnf1octb  45183  dvnprodlem1  45939  dvnprodlem2  45940  fouriersw  46224  vonval  46533  hoidmvlelem2  46589  hoidmvlelem3  46590  iccelpart  47429  uhgrimisgrgric  47926