Theorem rabex 4080

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

Syntax hints:   ∈ wcel 1481  {crab 2421  Vcvv 2689

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 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4054

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rab 2426  df-v 2691  df-in 3082  df-ss 3089

This theorem is referenced by:  repizf2  4094  undifexmid  4125  exmidexmid  4128  ordtriexmidlem  4443  ordtri2or2exmidlem  4449  onsucelsucexmidlem  4452  regexmid  4458  reg2exmid  4459  reg3exmid  4502  nnregexmid  4542  ssimaex  5490  acexmidlemcase  5777  acexmidlemv  5780  fnpm  6558  ssfiexmid  6778  domfiexmid  6780  inffiexmid  6808  ctssdclemr  7005  ctssexmid  7032  exmidonfinlem  7066  exmidaclem  7081  genpelvl  7344  genpelvu  7345  genipdm  7348  ltexprlemell  7430  ltexprlemelu  7431  cauappcvgprlemm  7477  cauappcvgprlemopl  7478  cauappcvgprlemlol  7479  cauappcvgprlemopu  7480  cauappcvgprlemupu  7481  cauappcvgprlemdisj  7483  cauappcvgprlemloc  7484  cauappcvgprlemladdfu  7486  cauappcvgprlemladdfl  7487  cauappcvgprlemladdru  7488  cauappcvgprlemladdrl  7489  cauappcvgprlem1  7491  cauappcvgprlem2  7492  caucvgprlemm  7500  caucvgprlemopl  7501  caucvgprlemlol  7502  caucvgprlemopu  7503  caucvgprlemupu  7504  caucvgprlemdisj  7506  caucvgprlemloc  7507  caucvgprlemladdfu  7509  caucvgprlem2  7512  caucvgprprlemell  7517  caucvgprprlemelu  7518  caucvgprprlemml  7526  caucvgprprlemmu  7527  caucvgprprlemexbt  7538  caucvgprprlem2  7542  suplocexprlem2b  7546  suplocexprlemlub  7556  sup3exmid  8739  dfuzi  9185  uzval  9352  ixxval  9709  fzval  9823  oddennn  11941  evenennn  11942  znnen  11947  ctiunct  11989  fncld  12306  xmetunirn  12566  limccl  12836  ellimc3apf  12837  subctctexmid  13369  nninfex  13380