Theorem rabex 4147

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 4146	. 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 4121

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  4162  undifexmid  4193  exmidexmid  4196  ordtriexmidlem  4518  ordtri2or2exmidlem  4525  onsucelsucexmidlem  4528  regexmid  4534  reg2exmid  4535  reg3exmid  4579  nnregexmid  4620  ssimaex  5577  mptrabex  5744  acexmidlemcase  5869  acexmidlemv  5872  fnpm  6655  ssfiexmid  6875  domfiexmid  6877  inffiexmid  6905  ctssdclemr  7110  nninfex  7119  ctssexmid  7147  exmidonfinlem  7191  exmidaclem  7206  genpelvl  7510  genpelvu  7511  genipdm  7514  ltexprlemell  7596  ltexprlemelu  7597  cauappcvgprlemm  7643  cauappcvgprlemopl  7644  cauappcvgprlemlol  7645  cauappcvgprlemopu  7646  cauappcvgprlemupu  7647  cauappcvgprlemdisj  7649  cauappcvgprlemloc  7650  cauappcvgprlemladdfu  7652  cauappcvgprlemladdfl  7653  cauappcvgprlemladdru  7654  cauappcvgprlemladdrl  7655  cauappcvgprlem1  7657  cauappcvgprlem2  7658  caucvgprlemm  7666  caucvgprlemopl  7667  caucvgprlemlol  7668  caucvgprlemopu  7669  caucvgprlemupu  7670  caucvgprlemdisj  7672  caucvgprlemloc  7673  caucvgprlemladdfu  7675  caucvgprlem2  7678  caucvgprprlemell  7683  caucvgprprlemelu  7684  caucvgprprlemml  7692  caucvgprprlemmu  7693  caucvgprprlemexbt  7704  caucvgprprlem2  7708  suplocexprlem2b  7712  suplocexprlemlub  7722  sup3exmid  8913  dfuzi  9362  uzval  9529  ixxval  9895  fzval  10009  oddennn  12392  evenennn  12393  znnen  12398  ctiunct  12440  fncld  13568  xmetunirn  13828  limccl  14098  ellimc3apf  14099  subctctexmid  14720