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  5881  acexmidlemcase  6012  acexmidlemv  6015  fnpm  6824  ssfiexmid  7062  ssfiexmidt  7064  domfiexmid  7066  inffiexmid  7097  ctssdclemr  7310  nninfex  7319  ctssexmid  7348  exmidonfinlem  7403  exmidaclem  7422  genpelvl  7731  genpelvu  7732  genipdm  7735  ltexprlemell  7817  ltexprlemelu  7818  cauappcvgprlemm  7864  cauappcvgprlemopl  7865  cauappcvgprlemlol  7866  cauappcvgprlemopu  7867  cauappcvgprlemupu  7868  cauappcvgprlemdisj  7870  cauappcvgprlemloc  7871  cauappcvgprlemladdfu  7873  cauappcvgprlemladdfl  7874  cauappcvgprlemladdru  7875  cauappcvgprlemladdrl  7876  cauappcvgprlem1  7878  cauappcvgprlem2  7879  caucvgprlemm  7887  caucvgprlemopl  7888  caucvgprlemlol  7889  caucvgprlemopu  7890  caucvgprlemupu  7891  caucvgprlemdisj  7893  caucvgprlemloc  7894  caucvgprlemladdfu  7896  caucvgprlem2  7899  caucvgprprlemell  7904  caucvgprprlemelu  7905  caucvgprprlemml  7913  caucvgprprlemmu  7914  caucvgprprlemexbt  7925  caucvgprprlem2  7929  suplocexprlem2b  7933  suplocexprlemlub  7943  sup3exmid  9136  dfuzi  9589  uzval  9756  ixxval  10130  fzval  10244  bitsfval  12502  oddennn  13012  evenennn  13013  znnen  13018  ctiunct  13060  rhmex  14170  metuex  14568  expghmap  14620  psrval  14679  fnpsr  14680  fnmpl  14706  fncld  14821  xmetunirn  15081  limccl  15382  ellimc3apf  15383  clwwlknon  16279  clwwlk0on0  16281  subctctexmid  16601