Theorem resex 5322

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

Hypothesis

Ref	Expression
resex.1

Assertion

Ref	Expression
resex

Proof of Theorem resex

Step	Hyp	Ref	Expression
1		resex.1	. 2
2		resexg 5321	. 2
3	1, 2	ax-mp 5	1

Syntax hints:  e.wcel 1818  cvv 3109  |`cres 5006

This theorem is referenced by:  tfrlem9a  7074  domunsncan  7637  sbthlem10  7656  mapunen  7706  php3  7723  ssfi  7760  marypha1lem  7913  infdifsn  8094  ackbij2lem3  8642  fin1a2lem7  8807  hashf1lem2  12505  ramub2  14532  resf1st  15263  resf2nd  15264  funcres  15265  lubfval  15608  glbfval  15621  znval  18572  znle  18573  usgrafis  24415  cusgrasize  24478  wlknwwlknvbij  24740  clwwlkvbij  24801  hhssva  26175  hhsssm  26176  hhssnm  26177  hhshsslem1  26183  eulerpartlemt  28310  eulerpartgbij  28311  eulerpart  28321  fibp1  28340  subfacp1lem3  28626  subfacp1lem5  28628  dfrdg2  29228  nofulllem5  29466  tfrqfree  29601  finixpnum  30038  mbfresfi  30061  sdclem2  30235  diophrex  30709  rexrabdioph  30727  2rexfrabdioph  30729  3rexfrabdioph  30730  4rexfrabdioph  30731  6rexfrabdioph  30732  7rexfrabdioph  30733  rmydioph  30956  rmxdioph  30958  expdiophlem2  30964  dvnprodlem1  31743  dvnprodlem2  31744  fouriersw  32014  uhgres  32379

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3482  df-ss 3489  df-res 5016