Theorem rabex 4234

Description: Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 19-Jul-1996.)

Hypothesis

Ref	Expression
rabex.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
rabex	⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rabex

Step	Hyp	Ref	Expression
1		rabex.1	. 2 ⊢ 𝐴 ∈ V
2		rabexg 4233	. 2 ⊢ (𝐴 ∈ V → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)
3	1, 2	ax-mp 5	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V

Syntax hints:   ∈ wcel 2202  {crab 2514  Vcvv 2802

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-sep 4207

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rab 2519  df-v 2804  df-in 3206  df-ss 3213

This theorem is referenced by:  rab2ex  4237  repizf2  4252  undifexmid  4283  exmidexmid  4286  ordtriexmidlem  4617  ordtri2or2exmidlem  4624  onsucelsucexmidlem  4627  regexmid  4633  reg2exmid  4634  reg3exmid  4678  nnregexmid  4719  ssimaex  5707  mptrabex  5882  acexmidlemcase  6013  acexmidlemv  6016  fnpm  6825  ssfiexmid  7063  ssfiexmidt  7065  domfiexmid  7067  inffiexmid  7098  ctssdclemr  7311  nninfex  7320  ctssexmid  7349  exmidonfinlem  7404  exmidaclem  7423  genpelvl  7732  genpelvu  7733  genipdm  7736  ltexprlemell  7818  ltexprlemelu  7819  cauappcvgprlemm  7865  cauappcvgprlemopl  7866  cauappcvgprlemlol  7867  cauappcvgprlemopu  7868  cauappcvgprlemupu  7869  cauappcvgprlemdisj  7871  cauappcvgprlemloc  7872  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  cauappcvgprlem1  7879  cauappcvgprlem2  7880  caucvgprlemm  7888  caucvgprlemopl  7889  caucvgprlemlol  7890  caucvgprlemopu  7891  caucvgprlemupu  7892  caucvgprlemdisj  7894  caucvgprlemloc  7895  caucvgprlemladdfu  7897  caucvgprlem2  7900  caucvgprprlemell  7905  caucvgprprlemelu  7906  caucvgprprlemml  7914  caucvgprprlemmu  7915  caucvgprprlemexbt  7926  caucvgprprlem2  7930  suplocexprlem2b  7934  suplocexprlemlub  7944  sup3exmid  9137  dfuzi  9590  uzval  9757  ixxval  10131  fzval  10245  bitsfval  12508  oddennn  13018  evenennn  13019  znnen  13024  ctiunct  13066  rhmex  14177  metuex  14575  expghmap  14627  psrval  14686  fnpsr  14687  fnmpl  14713  fncld  14828  xmetunirn  15088  limccl  15389  ellimc3apf  15390  clwwlknon  16286  clwwlk0on0  16288  subctctexmid  16627