Theorem rabex 4174

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 4173	. 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 2164   {crab 2476   _Vcvv 2760

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-sep 4148

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rab 2481  df-v 2762  df-in 3160  df-ss 3167

This theorem is referenced by:  rab2ex  4177  repizf2  4192  undifexmid  4223  exmidexmid  4226  ordtriexmidlem  4552  ordtri2or2exmidlem  4559  onsucelsucexmidlem  4562  regexmid  4568  reg2exmid  4569  reg3exmid  4613  nnregexmid  4654  ssimaex  5619  mptrabex  5787  acexmidlemcase  5914  acexmidlemv  5917  fnpm  6712  ssfiexmid  6934  domfiexmid  6936  inffiexmid  6964  ctssdclemr  7173  nninfex  7182  ctssexmid  7211  exmidonfinlem  7255  exmidaclem  7270  genpelvl  7574  genpelvu  7575  genipdm  7578  ltexprlemell  7660  ltexprlemelu  7661  cauappcvgprlemm  7707  cauappcvgprlemopl  7708  cauappcvgprlemlol  7709  cauappcvgprlemopu  7710  cauappcvgprlemupu  7711  cauappcvgprlemdisj  7713  cauappcvgprlemloc  7714  cauappcvgprlemladdfu  7716  cauappcvgprlemladdfl  7717  cauappcvgprlemladdru  7718  cauappcvgprlemladdrl  7719  cauappcvgprlem1  7721  cauappcvgprlem2  7722  caucvgprlemm  7730  caucvgprlemopl  7731  caucvgprlemlol  7732  caucvgprlemopu  7733  caucvgprlemupu  7734  caucvgprlemdisj  7736  caucvgprlemloc  7737  caucvgprlemladdfu  7739  caucvgprlem2  7742  caucvgprprlemell  7747  caucvgprprlemelu  7748  caucvgprprlemml  7756  caucvgprprlemmu  7757  caucvgprprlemexbt  7768  caucvgprprlem2  7772  suplocexprlem2b  7776  suplocexprlemlub  7786  sup3exmid  8978  dfuzi  9430  uzval  9597  ixxval  9965  fzval  10079  oddennn  12552  evenennn  12553  znnen  12558  ctiunct  12600  rhmex  13656  metuex  14054  expghmap  14106  psrval  14163  fnpsr  14164  fncld  14277  xmetunirn  14537  limccl  14838  ellimc3apf  14839  subctctexmid  15561