Theorem rabex 4030

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 4029	. 2 |- ( A e. _V -> { x e. A | ph } e. _V )
3	1, 2	ax-mp 7	1 |- { x e. A | ph } e. _V

Syntax hints:   e. wcel 1461   {crab 2392   _Vcvv 2655

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-sep 4004

This theorem depends on definitions:  df-bi 116  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-rab 2397  df-v 2657  df-in 3041  df-ss 3048

This theorem is referenced by:  repizf2  4044  undifexmid  4075  exmidexmid  4078  ordtriexmidlem  4393  ordtri2or2exmidlem  4399  onsucelsucexmidlem  4402  regexmid  4408  reg2exmid  4409  reg3exmid  4452  nnregexmid  4492  ssimaex  5434  acexmidlemcase  5721  acexmidlemv  5724  fnpm  6502  ssfiexmid  6721  domfiexmid  6723  inffiexmid  6751  ctssdclemr  6947  ctssexmid  6972  exmidaclem  7009  genpelvl  7262  genpelvu  7263  genipdm  7266  ltexprlemell  7348  ltexprlemelu  7349  cauappcvgprlemm  7395  cauappcvgprlemopl  7396  cauappcvgprlemlol  7397  cauappcvgprlemopu  7398  cauappcvgprlemupu  7399  cauappcvgprlemdisj  7401  cauappcvgprlemloc  7402  cauappcvgprlemladdfu  7404  cauappcvgprlemladdfl  7405  cauappcvgprlemladdru  7406  cauappcvgprlemladdrl  7407  cauappcvgprlem1  7409  cauappcvgprlem2  7410  caucvgprlemm  7418  caucvgprlemopl  7419  caucvgprlemlol  7420  caucvgprlemopu  7421  caucvgprlemupu  7422  caucvgprlemdisj  7424  caucvgprlemloc  7425  caucvgprlemladdfu  7427  caucvgprlem2  7430  caucvgprprlemell  7435  caucvgprprlemelu  7436  caucvgprprlemml  7444  caucvgprprlemmu  7445  caucvgprprlemexbt  7456  caucvgprprlem2  7460  sup3exmid  8619  dfuzi  9059  uzval  9224  ixxval  9566  fzval  9679  oddennn  11744  evenennn  11745  znnen  11750  ctiunct  11790  fncld  12104  xmetunirn  12341  limccl  12578  ellimc3apf  12579  nninfex  12886