Theorem rabex 4067

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 4066	. 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 1480   {crab 2418   _Vcvv 2681

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119  ax-sep 4041

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-rab 2423  df-v 2683  df-in 3072  df-ss 3079

This theorem is referenced by:  repizf2  4081  undifexmid  4112  exmidexmid  4115  ordtriexmidlem  4430  ordtri2or2exmidlem  4436  onsucelsucexmidlem  4439  regexmid  4445  reg2exmid  4446  reg3exmid  4489  nnregexmid  4529  ssimaex  5475  acexmidlemcase  5762  acexmidlemv  5765  fnpm  6543  ssfiexmid  6763  domfiexmid  6765  inffiexmid  6793  ctssdclemr  6990  ctssexmid  7017  exmidonfinlem  7042  exmidaclem  7057  genpelvl  7313  genpelvu  7314  genipdm  7317  ltexprlemell  7399  ltexprlemelu  7400  cauappcvgprlemm  7446  cauappcvgprlemopl  7447  cauappcvgprlemlol  7448  cauappcvgprlemopu  7449  cauappcvgprlemupu  7450  cauappcvgprlemdisj  7452  cauappcvgprlemloc  7453  cauappcvgprlemladdfu  7455  cauappcvgprlemladdfl  7456  cauappcvgprlemladdru  7457  cauappcvgprlemladdrl  7458  cauappcvgprlem1  7460  cauappcvgprlem2  7461  caucvgprlemm  7469  caucvgprlemopl  7470  caucvgprlemlol  7471  caucvgprlemopu  7472  caucvgprlemupu  7473  caucvgprlemdisj  7475  caucvgprlemloc  7476  caucvgprlemladdfu  7478  caucvgprlem2  7481  caucvgprprlemell  7486  caucvgprprlemelu  7487  caucvgprprlemml  7495  caucvgprprlemmu  7496  caucvgprprlemexbt  7507  caucvgprprlem2  7511  suplocexprlem2b  7515  suplocexprlemlub  7525  sup3exmid  8708  dfuzi  9154  uzval  9321  ixxval  9672  fzval  9785  oddennn  11894  evenennn  11895  znnen  11900  ctiunct  11942  fncld  12256  xmetunirn  12516  limccl  12786  ellimc3apf  12787  subctctexmid  13185  nninfex  13194