Theorem rabex 4239

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 4238	. 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 2202   {crab 2515   _Vcvv 2803

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-sep 4212

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rab 2520  df-v 2805  df-in 3207  df-ss 3214

This theorem is referenced by:  rab2ex  4242  repizf2  4258  undifexmid  4289  exmidexmid  4292  ordtriexmidlem  4623  ordtri2or2exmidlem  4630  onsucelsucexmidlem  4633  regexmid  4639  reg2exmid  4640  reg3exmid  4684  nnregexmid  4725  ssimaex  5716  mptrabex  5892  acexmidlemcase  6023  acexmidlemv  6026  fnpm  6868  ssfiexmid  7106  ssfiexmidt  7108  domfiexmid  7110  inffiexmid  7141  ctssdclemr  7371  nninfex  7380  ctssexmid  7409  exmidonfinlem  7464  exmidaclem  7483  genpelvl  7792  genpelvu  7793  genipdm  7796  ltexprlemell  7878  ltexprlemelu  7879  cauappcvgprlemm  7925  cauappcvgprlemopl  7926  cauappcvgprlemlol  7927  cauappcvgprlemopu  7928  cauappcvgprlemupu  7929  cauappcvgprlemdisj  7931  cauappcvgprlemloc  7932  cauappcvgprlemladdfu  7934  cauappcvgprlemladdfl  7935  cauappcvgprlemladdru  7936  cauappcvgprlemladdrl  7937  cauappcvgprlem1  7939  cauappcvgprlem2  7940  caucvgprlemm  7948  caucvgprlemopl  7949  caucvgprlemlol  7950  caucvgprlemopu  7951  caucvgprlemupu  7952  caucvgprlemdisj  7954  caucvgprlemloc  7955  caucvgprlemladdfu  7957  caucvgprlem2  7960  caucvgprprlemell  7965  caucvgprprlemelu  7966  caucvgprprlemml  7974  caucvgprprlemmu  7975  caucvgprprlemexbt  7986  caucvgprprlem2  7990  suplocexprlem2b  7994  suplocexprlemlub  8004  sup3exmid  9196  dfuzi  9651  uzval  9818  ixxval  10192  fzval  10307  bitsfval  12583  oddennn  13093  evenennn  13094  znnen  13099  ctiunct  13141  rhmex  14252  metuex  14651  expghmap  14703  psrval  14762  fnpsr  14763  fnmpl  14794  fncld  14909  xmetunirn  15169  limccl  15470  ellimc3apf  15471  clwwlknon  16370  clwwlk0on0  16372  subctctexmid  16722