Theorem rabex 4234

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 4233	. 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 2514   _Vcvv 2802

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-sep 4207

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rab 2519  df-v 2804  df-in 3206  df-ss 3213

This theorem is referenced by:  rab2ex  4237  repizf2  4252  undifexmid  4283  exmidexmid  4286  ordtriexmidlem  4617  ordtri2or2exmidlem  4624  onsucelsucexmidlem  4627  regexmid  4633  reg2exmid  4634  reg3exmid  4678  nnregexmid  4719  ssimaex  5708  mptrabex  5885  acexmidlemcase  6016  acexmidlemv  6019  fnpm  6828  ssfiexmid  7066  ssfiexmidt  7068  domfiexmid  7070  inffiexmid  7101  ctssdclemr  7314  nninfex  7323  ctssexmid  7352  exmidonfinlem  7407  exmidaclem  7426  genpelvl  7735  genpelvu  7736  genipdm  7739  ltexprlemell  7821  ltexprlemelu  7822  cauappcvgprlemm  7868  cauappcvgprlemopl  7869  cauappcvgprlemlol  7870  cauappcvgprlemopu  7871  cauappcvgprlemupu  7872  cauappcvgprlemdisj  7874  cauappcvgprlemloc  7875  cauappcvgprlemladdfu  7877  cauappcvgprlemladdfl  7878  cauappcvgprlemladdru  7879  cauappcvgprlemladdrl  7880  cauappcvgprlem1  7882  cauappcvgprlem2  7883  caucvgprlemm  7891  caucvgprlemopl  7892  caucvgprlemlol  7893  caucvgprlemopu  7894  caucvgprlemupu  7895  caucvgprlemdisj  7897  caucvgprlemloc  7898  caucvgprlemladdfu  7900  caucvgprlem2  7903  caucvgprprlemell  7908  caucvgprprlemelu  7909  caucvgprprlemml  7917  caucvgprprlemmu  7918  caucvgprprlemexbt  7929  caucvgprprlem2  7933  suplocexprlem2b  7937  suplocexprlemlub  7947  sup3exmid  9140  dfuzi  9593  uzval  9760  ixxval  10134  fzval  10248  bitsfval  12524  oddennn  13034  evenennn  13035  znnen  13040  ctiunct  13082  rhmex  14193  metuex  14591  expghmap  14643  psrval  14702  fnpsr  14703  fnmpl  14734  fncld  14849  xmetunirn  15109  limccl  15410  ellimc3apf  15411  clwwlknon  16307  clwwlk0on0  16309  subctctexmid  16660