Theorem rabex 4261

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 4260	. 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 4233

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 3220  df-ss 3227

This theorem is referenced by:  rab2ex  4264  repizf2  4280  undifexmid  4311  exmidexmid  4314  ordtriexmidlem  4646  ordtri2or2exmidlem  4653  onsucelsucexmidlem  4656  regexmid  4662  reg2exmid  4663  reg3exmid  4707  nnregexmid  4748  ssimaex  5743  mptrabex  5919  acexmidlemcase  6053  acexmidlemv  6056  fnpm  6903  ssfiexmid  7144  ssfiexmidt  7146  domfiexmid  7148  inffiexmid  7179  ctssdclemr  7416  nninfex  7425  ctssexmid  7454  exmidonfinlem  7509  exmidaclem  7528  genpelvl  7843  genpelvu  7844  genipdm  7847  ltexprlemell  7929  ltexprlemelu  7930  cauappcvgprlemm  7976  cauappcvgprlemopl  7977  cauappcvgprlemlol  7978  cauappcvgprlemopu  7979  cauappcvgprlemupu  7980  cauappcvgprlemdisj  7982  cauappcvgprlemloc  7983  cauappcvgprlemladdfu  7985  cauappcvgprlemladdfl  7986  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  cauappcvgprlem1  7990  cauappcvgprlem2  7991  caucvgprlemm  7999  caucvgprlemopl  8000  caucvgprlemlol  8001  caucvgprlemopu  8002  caucvgprlemupu  8003  caucvgprlemdisj  8005  caucvgprlemloc  8006  caucvgprlemladdfu  8008  caucvgprlem2  8011  caucvgprprlemell  8016  caucvgprprlemelu  8017  caucvgprprlemml  8025  caucvgprprlemmu  8026  caucvgprprlemexbt  8037  caucvgprprlem2  8041  suplocexprlem2b  8045  suplocexprlemlub  8055  sup3exmid  9248  dfuzi  9706  uzval  9873  ixxval  10248  fzval  10363  bitsfval  12653  ballotfilem8  13224  oddennn  13227  evenennn  13228  znnen  13233  ctiunct  13275  rhmex  14402  metuex  14829  expghmap  14881  psrval  14940  fnpsr  14941  fnmpl  14974  fncld  15089  xmetunirn  15349  limccl  15650  ellimc3apf  15651  clwwlknon  16550  clwwlk0on0  16552  subctctexmid  16900