Theorem rabex 4258

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 4257	. 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 2205   {crab 2526   _Vcvv 2815

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 2216  ax-sep 4230

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rab 2531  df-v 2817  df-in 3219  df-ss 3226

This theorem is referenced by:  rab2ex  4261  repizf2  4277  undifexmid  4308  exmidexmid  4311  ordtriexmidlem  4643  ordtri2or2exmidlem  4650  onsucelsucexmidlem  4653  regexmid  4659  reg2exmid  4660  reg3exmid  4704  nnregexmid  4745  ssimaex  5740  mptrabex  5916  acexmidlemcase  6047  acexmidlemv  6050  fnpm  6892  ssfiexmid  7133  ssfiexmidt  7135  domfiexmid  7137  inffiexmid  7168  ctssdclemr  7405  nninfex  7414  ctssexmid  7443  exmidonfinlem  7498  exmidaclem  7517  genpelvl  7829  genpelvu  7830  genipdm  7833  ltexprlemell  7915  ltexprlemelu  7916  cauappcvgprlemm  7962  cauappcvgprlemopl  7963  cauappcvgprlemlol  7964  cauappcvgprlemopu  7965  cauappcvgprlemupu  7966  cauappcvgprlemdisj  7968  cauappcvgprlemloc  7969  cauappcvgprlemladdfu  7971  cauappcvgprlemladdfl  7972  cauappcvgprlemladdru  7973  cauappcvgprlemladdrl  7974  cauappcvgprlem1  7976  cauappcvgprlem2  7977  caucvgprlemm  7985  caucvgprlemopl  7986  caucvgprlemlol  7987  caucvgprlemopu  7988  caucvgprlemupu  7989  caucvgprlemdisj  7991  caucvgprlemloc  7992  caucvgprlemladdfu  7994  caucvgprlem2  7997  caucvgprprlemell  8002  caucvgprprlemelu  8003  caucvgprprlemml  8011  caucvgprprlemmu  8012  caucvgprprlemexbt  8023  caucvgprprlem2  8027  suplocexprlem2b  8031  suplocexprlemlub  8041  sup3exmid  9233  dfuzi  9691  uzval  9858  ixxval  10232  fzval  10347  bitsfval  12632  oddennn  13160  evenennn  13161  znnen  13166  ctiunct  13208  rhmex  14319  metuex  14720  expghmap  14772  psrval  14831  fnpsr  14832  fnmpl  14865  fncld  14980  xmetunirn  15240  limccl  15541  ellimc3apf  15542  clwwlknon  16441  clwwlk0on0  16443  subctctexmid  16791