Theorem rabex 4196

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

Syntax hints:   ∈ wcel 2177  {crab 2489  Vcvv 2773

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-sep 4170

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-rab 2494  df-v 2775  df-in 3176  df-ss 3183

This theorem is referenced by:  rab2ex  4199  repizf2  4214  undifexmid  4245  exmidexmid  4248  ordtriexmidlem  4575  ordtri2or2exmidlem  4582  onsucelsucexmidlem  4585  regexmid  4591  reg2exmid  4592  reg3exmid  4636  nnregexmid  4677  ssimaex  5653  mptrabex  5825  acexmidlemcase  5952  acexmidlemv  5955  fnpm  6756  ssfiexmid  6988  domfiexmid  6990  inffiexmid  7018  ctssdclemr  7229  nninfex  7238  ctssexmid  7267  exmidonfinlem  7317  exmidaclem  7336  genpelvl  7645  genpelvu  7646  genipdm  7649  ltexprlemell  7731  ltexprlemelu  7732  cauappcvgprlemm  7778  cauappcvgprlemopl  7779  cauappcvgprlemlol  7780  cauappcvgprlemopu  7781  cauappcvgprlemupu  7782  cauappcvgprlemdisj  7784  cauappcvgprlemloc  7785  cauappcvgprlemladdfu  7787  cauappcvgprlemladdfl  7788  cauappcvgprlemladdru  7789  cauappcvgprlemladdrl  7790  cauappcvgprlem1  7792  cauappcvgprlem2  7793  caucvgprlemm  7801  caucvgprlemopl  7802  caucvgprlemlol  7803  caucvgprlemopu  7804  caucvgprlemupu  7805  caucvgprlemdisj  7807  caucvgprlemloc  7808  caucvgprlemladdfu  7810  caucvgprlem2  7813  caucvgprprlemell  7818  caucvgprprlemelu  7819  caucvgprprlemml  7827  caucvgprprlemmu  7828  caucvgprprlemexbt  7839  caucvgprprlem2  7843  suplocexprlem2b  7847  suplocexprlemlub  7857  sup3exmid  9050  dfuzi  9503  uzval  9670  ixxval  10038  fzval  10152  bitsfval  12328  oddennn  12838  evenennn  12839  znnen  12844  ctiunct  12886  rhmex  13994  metuex  14392  expghmap  14444  psrval  14503  fnpsr  14504  fnmpl  14530  fncld  14645  xmetunirn  14905  limccl  15206  ellimc3apf  15207  subctctexmid  16078