Theorem rabex 4145

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 4144	. 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 2148   {crab 2459   _Vcvv 2737

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-sep 4119

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rab 2464  df-v 2739  df-in 3135  df-ss 3142

This theorem is referenced by:  repizf2  4160  undifexmid  4191  exmidexmid  4194  ordtriexmidlem  4516  ordtri2or2exmidlem  4523  onsucelsucexmidlem  4526  regexmid  4532  reg2exmid  4533  reg3exmid  4577  nnregexmid  4618  ssimaex  5574  mptrabex  5741  acexmidlemcase  5865  acexmidlemv  5868  fnpm  6651  ssfiexmid  6871  domfiexmid  6873  inffiexmid  6901  ctssdclemr  7106  nninfex  7115  ctssexmid  7143  exmidonfinlem  7187  exmidaclem  7202  genpelvl  7506  genpelvu  7507  genipdm  7510  ltexprlemell  7592  ltexprlemelu  7593  cauappcvgprlemm  7639  cauappcvgprlemopl  7640  cauappcvgprlemlol  7641  cauappcvgprlemopu  7642  cauappcvgprlemupu  7643  cauappcvgprlemdisj  7645  cauappcvgprlemloc  7646  cauappcvgprlemladdfu  7648  cauappcvgprlemladdfl  7649  cauappcvgprlemladdru  7650  cauappcvgprlemladdrl  7651  cauappcvgprlem1  7653  cauappcvgprlem2  7654  caucvgprlemm  7662  caucvgprlemopl  7663  caucvgprlemlol  7664  caucvgprlemopu  7665  caucvgprlemupu  7666  caucvgprlemdisj  7668  caucvgprlemloc  7669  caucvgprlemladdfu  7671  caucvgprlem2  7674  caucvgprprlemell  7679  caucvgprprlemelu  7680  caucvgprprlemml  7688  caucvgprprlemmu  7689  caucvgprprlemexbt  7700  caucvgprprlem2  7704  suplocexprlem2b  7708  suplocexprlemlub  7718  sup3exmid  8908  dfuzi  9357  uzval  9524  ixxval  9890  fzval  10004  oddennn  12383  evenennn  12384  znnen  12389  ctiunct  12431  fncld  13380  xmetunirn  13640  limccl  13910  ellimc3apf  13911  subctctexmid  14521