Theorem rabex 4227

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 4226	. 2 ⊢ (𝐴 ∈ V → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)
3	1, 2	ax-mp 5	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V

Syntax hints:   ∈ wcel 2200  {crab 2512  Vcvv 2799

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4201

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rab 2517  df-v 2801  df-in 3203  df-ss 3210

This theorem is referenced by:  rab2ex  4230  repizf2  4245  undifexmid  4276  exmidexmid  4279  ordtriexmidlem  4610  ordtri2or2exmidlem  4617  onsucelsucexmidlem  4620  regexmid  4626  reg2exmid  4627  reg3exmid  4671  nnregexmid  4712  ssimaex  5694  mptrabex  5866  acexmidlemcase  5995  acexmidlemv  5998  fnpm  6801  ssfiexmid  7034  domfiexmid  7036  inffiexmid  7064  ctssdclemr  7275  nninfex  7284  ctssexmid  7313  exmidonfinlem  7367  exmidaclem  7386  genpelvl  7695  genpelvu  7696  genipdm  7699  ltexprlemell  7781  ltexprlemelu  7782  cauappcvgprlemm  7828  cauappcvgprlemopl  7829  cauappcvgprlemlol  7830  cauappcvgprlemopu  7831  cauappcvgprlemupu  7832  cauappcvgprlemdisj  7834  cauappcvgprlemloc  7835  cauappcvgprlemladdfu  7837  cauappcvgprlemladdfl  7838  cauappcvgprlemladdru  7839  cauappcvgprlemladdrl  7840  cauappcvgprlem1  7842  cauappcvgprlem2  7843  caucvgprlemm  7851  caucvgprlemopl  7852  caucvgprlemlol  7853  caucvgprlemopu  7854  caucvgprlemupu  7855  caucvgprlemdisj  7857  caucvgprlemloc  7858  caucvgprlemladdfu  7860  caucvgprlem2  7863  caucvgprprlemell  7868  caucvgprprlemelu  7869  caucvgprprlemml  7877  caucvgprprlemmu  7878  caucvgprprlemexbt  7889  caucvgprprlem2  7893  suplocexprlem2b  7897  suplocexprlemlub  7907  sup3exmid  9100  dfuzi  9553  uzval  9720  ixxval  10088  fzval  10202  bitsfval  12448  oddennn  12958  evenennn  12959  znnen  12964  ctiunct  13006  rhmex  14115  metuex  14513  expghmap  14565  psrval  14624  fnpsr  14625  fnmpl  14651  fncld  14766  xmetunirn  15026  limccl  15327  ellimc3apf  15328  subctctexmid  16325