Theorem rabex 4131

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

Syntax hints:   ∈ wcel 2141  {crab 2452  Vcvv 2730

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-sep 4105

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-rab 2457  df-v 2732  df-in 3127  df-ss 3134

This theorem is referenced by:  repizf2  4146  undifexmid  4177  exmidexmid  4180  ordtriexmidlem  4501  ordtri2or2exmidlem  4508  onsucelsucexmidlem  4511  regexmid  4517  reg2exmid  4518  reg3exmid  4562  nnregexmid  4603  ssimaex  5555  mptrabex  5721  acexmidlemcase  5845  acexmidlemv  5848  fnpm  6630  ssfiexmid  6850  domfiexmid  6852  inffiexmid  6880  ctssdclemr  7085  nninfex  7094  ctssexmid  7122  exmidonfinlem  7157  exmidaclem  7172  genpelvl  7461  genpelvu  7462  genipdm  7465  ltexprlemell  7547  ltexprlemelu  7548  cauappcvgprlemm  7594  cauappcvgprlemopl  7595  cauappcvgprlemlol  7596  cauappcvgprlemopu  7597  cauappcvgprlemupu  7598  cauappcvgprlemdisj  7600  cauappcvgprlemloc  7601  cauappcvgprlemladdfu  7603  cauappcvgprlemladdfl  7604  cauappcvgprlemladdru  7605  cauappcvgprlemladdrl  7606  cauappcvgprlem1  7608  cauappcvgprlem2  7609  caucvgprlemm  7617  caucvgprlemopl  7618  caucvgprlemlol  7619  caucvgprlemopu  7620  caucvgprlemupu  7621  caucvgprlemdisj  7623  caucvgprlemloc  7624  caucvgprlemladdfu  7626  caucvgprlem2  7629  caucvgprprlemell  7634  caucvgprprlemelu  7635  caucvgprprlemml  7643  caucvgprprlemmu  7644  caucvgprprlemexbt  7655  caucvgprprlem2  7659  suplocexprlem2b  7663  suplocexprlemlub  7673  sup3exmid  8860  dfuzi  9309  uzval  9476  ixxval  9840  fzval  9954  oddennn  12334  evenennn  12335  znnen  12340  ctiunct  12382  fncld  12851  xmetunirn  13111  limccl  13381  ellimc3apf  13382  subctctexmid  13994