Theorem rabex 4165

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

Syntax hints:   ∈ wcel 2160  {crab 2472  Vcvv 2752

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171  ax-sep 4139

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-rab 2477  df-v 2754  df-in 3150  df-ss 3157

This theorem is referenced by:  rab2ex  4168  repizf2  4183  undifexmid  4214  exmidexmid  4217  ordtriexmidlem  4539  ordtri2or2exmidlem  4546  onsucelsucexmidlem  4549  regexmid  4555  reg2exmid  4556  reg3exmid  4600  nnregexmid  4641  ssimaex  5601  mptrabex  5768  acexmidlemcase  5895  acexmidlemv  5898  fnpm  6686  ssfiexmid  6908  domfiexmid  6910  inffiexmid  6938  ctssdclemr  7145  nninfex  7154  ctssexmid  7183  exmidonfinlem  7227  exmidaclem  7242  genpelvl  7546  genpelvu  7547  genipdm  7550  ltexprlemell  7632  ltexprlemelu  7633  cauappcvgprlemm  7679  cauappcvgprlemopl  7680  cauappcvgprlemlol  7681  cauappcvgprlemopu  7682  cauappcvgprlemupu  7683  cauappcvgprlemdisj  7685  cauappcvgprlemloc  7686  cauappcvgprlemladdfu  7688  cauappcvgprlemladdfl  7689  cauappcvgprlemladdru  7690  cauappcvgprlemladdrl  7691  cauappcvgprlem1  7693  cauappcvgprlem2  7694  caucvgprlemm  7702  caucvgprlemopl  7703  caucvgprlemlol  7704  caucvgprlemopu  7705  caucvgprlemupu  7706  caucvgprlemdisj  7708  caucvgprlemloc  7709  caucvgprlemladdfu  7711  caucvgprlem2  7714  caucvgprprlemell  7719  caucvgprprlemelu  7720  caucvgprprlemml  7728  caucvgprprlemmu  7729  caucvgprprlemexbt  7740  caucvgprprlem2  7744  suplocexprlem2b  7748  suplocexprlemlub  7758  sup3exmid  8949  dfuzi  9398  uzval  9565  ixxval  9932  fzval  10046  oddennn  12454  evenennn  12455  znnen  12460  ctiunct  12502  rhmex  13532  psrval  13969  fnpsr  13970  fncld  14083  xmetunirn  14343  limccl  14613  ellimc3apf  14614  subctctexmid  15237