Theorem rabex 4120

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 4119	. 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 2135   {crab 2446   _Vcvv 2721

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 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146  ax-sep 4094

This theorem depends on definitions:  df-bi 116  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-rab 2451  df-v 2723  df-in 3117  df-ss 3124

This theorem is referenced by:  repizf2  4135  undifexmid  4166  exmidexmid  4169  ordtriexmidlem  4490  ordtri2or2exmidlem  4497  onsucelsucexmidlem  4500  regexmid  4506  reg2exmid  4507  reg3exmid  4551  nnregexmid  4592  ssimaex  5541  mptrabex  5707  acexmidlemcase  5831  acexmidlemv  5834  fnpm  6613  ssfiexmid  6833  domfiexmid  6835  inffiexmid  6863  ctssdclemr  7068  nninfex  7077  ctssexmid  7105  exmidonfinlem  7140  exmidaclem  7155  genpelvl  7444  genpelvu  7445  genipdm  7448  ltexprlemell  7530  ltexprlemelu  7531  cauappcvgprlemm  7577  cauappcvgprlemopl  7578  cauappcvgprlemlol  7579  cauappcvgprlemopu  7580  cauappcvgprlemupu  7581  cauappcvgprlemdisj  7583  cauappcvgprlemloc  7584  cauappcvgprlemladdfu  7586  cauappcvgprlemladdfl  7587  cauappcvgprlemladdru  7588  cauappcvgprlemladdrl  7589  cauappcvgprlem1  7591  cauappcvgprlem2  7592  caucvgprlemm  7600  caucvgprlemopl  7601  caucvgprlemlol  7602  caucvgprlemopu  7603  caucvgprlemupu  7604  caucvgprlemdisj  7606  caucvgprlemloc  7607  caucvgprlemladdfu  7609  caucvgprlem2  7612  caucvgprprlemell  7617  caucvgprprlemelu  7618  caucvgprprlemml  7626  caucvgprprlemmu  7627  caucvgprprlemexbt  7638  caucvgprprlem2  7642  suplocexprlem2b  7646  suplocexprlemlub  7656  sup3exmid  8843  dfuzi  9292  uzval  9459  ixxval  9823  fzval  9937  oddennn  12262  evenennn  12263  znnen  12268  ctiunct  12310  fncld  12639  xmetunirn  12899  limccl  13169  ellimc3apf  13170  subctctexmid  13715