Theorem rabex 4187

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

Syntax hints:   ∈ wcel 2175  {crab 2487  Vcvv 2771

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186  ax-sep 4161

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-rab 2492  df-v 2773  df-in 3171  df-ss 3178

This theorem is referenced by:  rab2ex  4190  repizf2  4205  undifexmid  4236  exmidexmid  4239  ordtriexmidlem  4565  ordtri2or2exmidlem  4572  onsucelsucexmidlem  4575  regexmid  4581  reg2exmid  4582  reg3exmid  4626  nnregexmid  4667  ssimaex  5634  mptrabex  5802  acexmidlemcase  5929  acexmidlemv  5932  fnpm  6733  ssfiexmid  6955  domfiexmid  6957  inffiexmid  6985  ctssdclemr  7196  nninfex  7205  ctssexmid  7234  exmidonfinlem  7283  exmidaclem  7302  genpelvl  7607  genpelvu  7608  genipdm  7611  ltexprlemell  7693  ltexprlemelu  7694  cauappcvgprlemm  7740  cauappcvgprlemopl  7741  cauappcvgprlemlol  7742  cauappcvgprlemopu  7743  cauappcvgprlemupu  7744  cauappcvgprlemdisj  7746  cauappcvgprlemloc  7747  cauappcvgprlemladdfu  7749  cauappcvgprlemladdfl  7750  cauappcvgprlemladdru  7751  cauappcvgprlemladdrl  7752  cauappcvgprlem1  7754  cauappcvgprlem2  7755  caucvgprlemm  7763  caucvgprlemopl  7764  caucvgprlemlol  7765  caucvgprlemopu  7766  caucvgprlemupu  7767  caucvgprlemdisj  7769  caucvgprlemloc  7770  caucvgprlemladdfu  7772  caucvgprlem2  7775  caucvgprprlemell  7780  caucvgprprlemelu  7781  caucvgprprlemml  7789  caucvgprprlemmu  7790  caucvgprprlemexbt  7801  caucvgprprlem2  7805  suplocexprlem2b  7809  suplocexprlemlub  7819  sup3exmid  9012  dfuzi  9465  uzval  9632  ixxval  10000  fzval  10114  bitsfval  12172  oddennn  12682  evenennn  12683  znnen  12688  ctiunct  12730  rhmex  13837  metuex  14235  expghmap  14287  psrval  14346  fnpsr  14347  fnmpl  14373  fncld  14488  xmetunirn  14748  limccl  15049  ellimc3apf  15050  subctctexmid  15801