Theorem rabex 4204

Description: Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 19-Jul-1996.)

Hypothesis

Ref	Expression
rabex.1	|- A e. _V

Assertion

Ref	Expression
rabex	|- { x e. A | ph } e. _V

Distinct variable group:   x, A

Allowed substitution hint:   ph( x)

Proof of Theorem rabex

Step	Hyp	Ref	Expression
1		rabex.1	. 2 |- A e. _V
2		rabexg 4203	. 2 |- ( A e. _V -> { x e. A | ph } e. _V )
3	1, 2	ax-mp 5	1 |- { x e. A | ph } e. _V

Syntax hints:   e. wcel 2178   {crab 2490   _Vcvv 2776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189  ax-sep 4178

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-rab 2495  df-v 2778  df-in 3180  df-ss 3187

This theorem is referenced by:  rab2ex  4207  repizf2  4222  undifexmid  4253  exmidexmid  4256  ordtriexmidlem  4585  ordtri2or2exmidlem  4592  onsucelsucexmidlem  4595  regexmid  4601  reg2exmid  4602  reg3exmid  4646  nnregexmid  4687  ssimaex  5663  mptrabex  5835  acexmidlemcase  5962  acexmidlemv  5965  fnpm  6766  ssfiexmid  6999  domfiexmid  7001  inffiexmid  7029  ctssdclemr  7240  nninfex  7249  ctssexmid  7278  exmidonfinlem  7332  exmidaclem  7351  genpelvl  7660  genpelvu  7661  genipdm  7664  ltexprlemell  7746  ltexprlemelu  7747  cauappcvgprlemm  7793  cauappcvgprlemopl  7794  cauappcvgprlemlol  7795  cauappcvgprlemopu  7796  cauappcvgprlemupu  7797  cauappcvgprlemdisj  7799  cauappcvgprlemloc  7800  cauappcvgprlemladdfu  7802  cauappcvgprlemladdfl  7803  cauappcvgprlemladdru  7804  cauappcvgprlemladdrl  7805  cauappcvgprlem1  7807  cauappcvgprlem2  7808  caucvgprlemm  7816  caucvgprlemopl  7817  caucvgprlemlol  7818  caucvgprlemopu  7819  caucvgprlemupu  7820  caucvgprlemdisj  7822  caucvgprlemloc  7823  caucvgprlemladdfu  7825  caucvgprlem2  7828  caucvgprprlemell  7833  caucvgprprlemelu  7834  caucvgprprlemml  7842  caucvgprprlemmu  7843  caucvgprprlemexbt  7854  caucvgprprlem2  7858  suplocexprlem2b  7862  suplocexprlemlub  7872  sup3exmid  9065  dfuzi  9518  uzval  9685  ixxval  10053  fzval  10167  bitsfval  12368  oddennn  12878  evenennn  12879  znnen  12884  ctiunct  12926  rhmex  14034  metuex  14432  expghmap  14484  psrval  14543  fnpsr  14544  fnmpl  14570  fncld  14685  xmetunirn  14945  limccl  15246  ellimc3apf  15247  subctctexmid  16139