Theorem rabex 4178

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

Syntax hints:   ∈ wcel 2167  {crab 2479  Vcvv 2763

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-sep 4152

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rab 2484  df-v 2765  df-in 3163  df-ss 3170

This theorem is referenced by:  rab2ex  4181  repizf2  4196  undifexmid  4227  exmidexmid  4230  ordtriexmidlem  4556  ordtri2or2exmidlem  4563  onsucelsucexmidlem  4566  regexmid  4572  reg2exmid  4573  reg3exmid  4617  nnregexmid  4658  ssimaex  5625  mptrabex  5793  acexmidlemcase  5920  acexmidlemv  5923  fnpm  6724  ssfiexmid  6946  domfiexmid  6948  inffiexmid  6976  ctssdclemr  7187  nninfex  7196  ctssexmid  7225  exmidonfinlem  7272  exmidaclem  7291  genpelvl  7596  genpelvu  7597  genipdm  7600  ltexprlemell  7682  ltexprlemelu  7683  cauappcvgprlemm  7729  cauappcvgprlemopl  7730  cauappcvgprlemlol  7731  cauappcvgprlemopu  7732  cauappcvgprlemupu  7733  cauappcvgprlemdisj  7735  cauappcvgprlemloc  7736  cauappcvgprlemladdfu  7738  cauappcvgprlemladdfl  7739  cauappcvgprlemladdru  7740  cauappcvgprlemladdrl  7741  cauappcvgprlem1  7743  cauappcvgprlem2  7744  caucvgprlemm  7752  caucvgprlemopl  7753  caucvgprlemlol  7754  caucvgprlemopu  7755  caucvgprlemupu  7756  caucvgprlemdisj  7758  caucvgprlemloc  7759  caucvgprlemladdfu  7761  caucvgprlem2  7764  caucvgprprlemell  7769  caucvgprprlemelu  7770  caucvgprprlemml  7778  caucvgprprlemmu  7779  caucvgprprlemexbt  7790  caucvgprprlem2  7794  suplocexprlem2b  7798  suplocexprlemlub  7808  sup3exmid  9001  dfuzi  9453  uzval  9620  ixxval  9988  fzval  10102  bitsfval  12124  oddennn  12634  evenennn  12635  znnen  12640  ctiunct  12682  rhmex  13789  metuex  14187  expghmap  14239  psrval  14296  fnpsr  14297  fncld  14418  xmetunirn  14678  limccl  14979  ellimc3apf  14980  subctctexmid  15731