Theorem rabex 4275

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 4274	. 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 2209   {crab 2532   _Vcvv 2821

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-sep 4244

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rab 2537  df-v 2823  df-in 3226  df-ss 3233

This theorem is referenced by:  rab2ex  4278  repizf2  4294  undifexmid  4325  exmidexmid  4328  ordtriexmidlem  4661  ordtri2or2exmidlem  4668  onsucelsucexmidlem  4671  regexmid  4677  reg2exmid  4678  reg3exmid  4722  nnregexmid  4763  ssimaex  5758  mptrabex  5936  acexmidlemcase  6070  acexmidlemv  6073  fnpm  6920  ssfiexmid  7168  ssfiexmidt  7170  domfiexmid  7172  inffiexmid  7203  ctssdclemr  7442  nninfex  7451  ctssexmid  7480  exmidonfinlem  7535  exmidaclem  7554  genpelvl  7869  genpelvu  7870  genipdm  7873  ltexprlemell  7955  ltexprlemelu  7956  cauappcvgprlemm  8002  cauappcvgprlemopl  8003  cauappcvgprlemlol  8004  cauappcvgprlemopu  8005  cauappcvgprlemupu  8006  cauappcvgprlemdisj  8008  cauappcvgprlemloc  8009  cauappcvgprlemladdfu  8011  cauappcvgprlemladdfl  8012  cauappcvgprlemladdru  8013  cauappcvgprlemladdrl  8014  cauappcvgprlem1  8016  cauappcvgprlem2  8017  caucvgprlemm  8025  caucvgprlemopl  8026  caucvgprlemlol  8027  caucvgprlemopu  8028  caucvgprlemupu  8029  caucvgprlemdisj  8031  caucvgprlemloc  8032  caucvgprlemladdfu  8034  caucvgprlem2  8037  caucvgprprlemell  8042  caucvgprprlemelu  8043  caucvgprprlemml  8051  caucvgprprlemmu  8052  caucvgprprlemexbt  8063  caucvgprprlem2  8067  suplocexprlem2b  8071  suplocexprlemlub  8081  sup3exmid  9277  dfuzi  9735  uzval  9902  ixxval  10277  fzval  10392  bitsfval  12687  ballotfilem8  13258  oddennn  13261  evenennn  13262  znnen  13267  ctiunct  13309  rhmex  14437  metuex  14864  expghmap  14914  psrval  14973  fnpsr  14974  fnmpl  15007  fncld  15122  xmetunirn  15382  limccl  15683  ellimc3apf  15684  clwwlknon  16584  clwwlk0on0  16586  subctctexmid  16944