Theorem resex 5443

Description: The restriction of a set is a set. (Contributed by Jeff Madsen, 19-Jun-2011.)

Hypothesis

Ref	Expression
resex.1	|- A e. _V

Assertion

Ref	Expression
resex	|- ( A |` B ) e. _V

Proof of Theorem resex

Step	Hyp	Ref	Expression
1		resex.1	. 2 |- A e. _V
2		resexg 5442	. 2 |- ( A e. _V -> ( A |` B ) e. _V )
3	1, 2	ax-mp 5	1 |- ( A |` B ) e. _V

Syntax hints:   e. wcel 1990   _Vcvv 3200   |` cres 5116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ss 3588  df-res 5126

This theorem is referenced by:  wfrlem17  7431  tfrlem9a  7482  domunsncan  8060  sbthlem10  8079  mapunen  8129  php3  8146  ssfi  8180  marypha1lem  8339  infdifsn  8554  ackbij2lem3  9063  fin1a2lem7  9228  hashf1lem2  13240  ramub2  15718  resf1st  16554  resf2nd  16555  funcres  16556  lubfval  16978  glbfval  16991  znval  19883  znle  19884  uhgrspanop  26188  upgrspanop  26189  umgrspanop  26190  usgrspanop  26191  uhgrspan1lem1  26192  vtxdginducedm1lem1  26435  vtxdginducedm1fi  26440  finsumvtxdg2ssteplem4  26444  finsumvtxdg2size  26446  wlksnwwlknvbij  26803  clwwlksvbij  26922  eupthvdres  27095  eupth2lem3  27096  eupth2lemb  27097  hhssva  28114  hhsssm  28115  hhssnm  28116  hhshsslem1  28124  eulerpartlemt  30433  eulerpartgbij  30434  eulerpart  30444  fibp1  30463  actfunsnf1o  30682  subfacp1lem3  31164  subfacp1lem5  31166  dfrdg2  31701  dfrecs2  32057  finixpnum  33394  poimirlem4  33413  poimirlem9  33418  mbfresfi  33456  sdclem2  33538  diophrex  37339  rexrabdioph  37358  2rexfrabdioph  37360  3rexfrabdioph  37361  4rexfrabdioph  37362  6rexfrabdioph  37363  7rexfrabdioph  37364  rmydioph  37581  rmxdioph  37583  expdiophlem2  37589  ssnnf1octb  39382  dvnprodlem1  40161  dvnprodlem2  40162  fouriersw  40448  vonval  40754  hoidmvlelem2  40810  hoidmvlelem3  40811  iccelpart  41369