Theorem rabex 4133

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 4132	. 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 4107

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  4148  undifexmid  4179  exmidexmid  4182  ordtriexmidlem  4503  ordtri2or2exmidlem  4510  onsucelsucexmidlem  4513  regexmid  4519  reg2exmid  4520  reg3exmid  4564  nnregexmid  4605  ssimaex  5557  mptrabex  5724  acexmidlemcase  5848  acexmidlemv  5851  fnpm  6634  ssfiexmid  6854  domfiexmid  6856  inffiexmid  6884  ctssdclemr  7089  nninfex  7098  ctssexmid  7126  exmidonfinlem  7170  exmidaclem  7185  genpelvl  7474  genpelvu  7475  genipdm  7478  ltexprlemell  7560  ltexprlemelu  7561  cauappcvgprlemm  7607  cauappcvgprlemopl  7608  cauappcvgprlemlol  7609  cauappcvgprlemopu  7610  cauappcvgprlemupu  7611  cauappcvgprlemdisj  7613  cauappcvgprlemloc  7614  cauappcvgprlemladdfu  7616  cauappcvgprlemladdfl  7617  cauappcvgprlemladdru  7618  cauappcvgprlemladdrl  7619  cauappcvgprlem1  7621  cauappcvgprlem2  7622  caucvgprlemm  7630  caucvgprlemopl  7631  caucvgprlemlol  7632  caucvgprlemopu  7633  caucvgprlemupu  7634  caucvgprlemdisj  7636  caucvgprlemloc  7637  caucvgprlemladdfu  7639  caucvgprlem2  7642  caucvgprprlemell  7647  caucvgprprlemelu  7648  caucvgprprlemml  7656  caucvgprprlemmu  7657  caucvgprprlemexbt  7668  caucvgprprlem2  7672  suplocexprlem2b  7676  suplocexprlemlub  7686  sup3exmid  8873  dfuzi  9322  uzval  9489  ixxval  9853  fzval  9967  oddennn  12347  evenennn  12348  znnen  12353  ctiunct  12395  fncld  12892  xmetunirn  13152  limccl  13422  ellimc3apf  13423  subctctexmid  14034