Theorem rabex 4149

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 4148	. 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 2148   {crab 2459   _Vcvv 2739

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-sep 4123

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rab 2464  df-v 2741  df-in 3137  df-ss 3144

This theorem is referenced by:  repizf2  4164  undifexmid  4195  exmidexmid  4198  ordtriexmidlem  4520  ordtri2or2exmidlem  4527  onsucelsucexmidlem  4530  regexmid  4536  reg2exmid  4537  reg3exmid  4581  nnregexmid  4622  ssimaex  5579  mptrabex  5746  acexmidlemcase  5872  acexmidlemv  5875  fnpm  6658  ssfiexmid  6878  domfiexmid  6880  inffiexmid  6908  ctssdclemr  7113  nninfex  7122  ctssexmid  7150  exmidonfinlem  7194  exmidaclem  7209  genpelvl  7513  genpelvu  7514  genipdm  7517  ltexprlemell  7599  ltexprlemelu  7600  cauappcvgprlemm  7646  cauappcvgprlemopl  7647  cauappcvgprlemlol  7648  cauappcvgprlemopu  7649  cauappcvgprlemupu  7650  cauappcvgprlemdisj  7652  cauappcvgprlemloc  7653  cauappcvgprlemladdfu  7655  cauappcvgprlemladdfl  7656  cauappcvgprlemladdru  7657  cauappcvgprlemladdrl  7658  cauappcvgprlem1  7660  cauappcvgprlem2  7661  caucvgprlemm  7669  caucvgprlemopl  7670  caucvgprlemlol  7671  caucvgprlemopu  7672  caucvgprlemupu  7673  caucvgprlemdisj  7675  caucvgprlemloc  7676  caucvgprlemladdfu  7678  caucvgprlem2  7681  caucvgprprlemell  7686  caucvgprprlemelu  7687  caucvgprprlemml  7695  caucvgprprlemmu  7696  caucvgprprlemexbt  7707  caucvgprprlem2  7711  suplocexprlem2b  7715  suplocexprlemlub  7725  sup3exmid  8916  dfuzi  9365  uzval  9532  ixxval  9898  fzval  10012  oddennn  12395  evenennn  12396  znnen  12401  ctiunct  12443  fncld  13683  xmetunirn  13943  limccl  14213  ellimc3apf  14214  subctctexmid  14835