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  4566  ordtri2or2exmidlem  4573  onsucelsucexmidlem  4576  regexmid  4582  reg2exmid  4583  reg3exmid  4627  nnregexmid  4668  ssimaex  5639  mptrabex  5811  acexmidlemcase  5938  acexmidlemv  5941  fnpm  6742  ssfiexmid  6972  domfiexmid  6974  inffiexmid  7002  ctssdclemr  7213  nninfex  7222  ctssexmid  7251  exmidonfinlem  7300  exmidaclem  7319  genpelvl  7624  genpelvu  7625  genipdm  7628  ltexprlemell  7710  ltexprlemelu  7711  cauappcvgprlemm  7757  cauappcvgprlemopl  7758  cauappcvgprlemlol  7759  cauappcvgprlemopu  7760  cauappcvgprlemupu  7761  cauappcvgprlemdisj  7763  cauappcvgprlemloc  7764  cauappcvgprlemladdfu  7766  cauappcvgprlemladdfl  7767  cauappcvgprlemladdru  7768  cauappcvgprlemladdrl  7769  cauappcvgprlem1  7771  cauappcvgprlem2  7772  caucvgprlemm  7780  caucvgprlemopl  7781  caucvgprlemlol  7782  caucvgprlemopu  7783  caucvgprlemupu  7784  caucvgprlemdisj  7786  caucvgprlemloc  7787  caucvgprlemladdfu  7789  caucvgprlem2  7792  caucvgprprlemell  7797  caucvgprprlemelu  7798  caucvgprprlemml  7806  caucvgprprlemmu  7807  caucvgprprlemexbt  7818  caucvgprprlem2  7822  suplocexprlem2b  7826  suplocexprlemlub  7836  sup3exmid  9029  dfuzi  9482  uzval  9649  ixxval  10017  fzval  10131  bitsfval  12195  oddennn  12705  evenennn  12706  znnen  12711  ctiunct  12753  rhmex  13861  metuex  14259  expghmap  14311  psrval  14370  fnpsr  14371  fnmpl  14397  fncld  14512  xmetunirn  14772  limccl  15073  ellimc3apf  15074  subctctexmid  15870