Theorem rabex 4125

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

Syntax hints:   ∈ wcel 2136  {crab 2447  Vcvv 2725

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147  ax-sep 4099

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-rab 2452  df-v 2727  df-in 3121  df-ss 3128

This theorem is referenced by:  repizf2  4140  undifexmid  4171  exmidexmid  4174  ordtriexmidlem  4495  ordtri2or2exmidlem  4502  onsucelsucexmidlem  4505  regexmid  4511  reg2exmid  4512  reg3exmid  4556  nnregexmid  4597  ssimaex  5546  mptrabex  5712  acexmidlemcase  5836  acexmidlemv  5839  fnpm  6618  ssfiexmid  6838  domfiexmid  6840  inffiexmid  6868  ctssdclemr  7073  nninfex  7082  ctssexmid  7110  exmidonfinlem  7145  exmidaclem  7160  genpelvl  7449  genpelvu  7450  genipdm  7453  ltexprlemell  7535  ltexprlemelu  7536  cauappcvgprlemm  7582  cauappcvgprlemopl  7583  cauappcvgprlemlol  7584  cauappcvgprlemopu  7585  cauappcvgprlemupu  7586  cauappcvgprlemdisj  7588  cauappcvgprlemloc  7589  cauappcvgprlemladdfu  7591  cauappcvgprlemladdfl  7592  cauappcvgprlemladdru  7593  cauappcvgprlemladdrl  7594  cauappcvgprlem1  7596  cauappcvgprlem2  7597  caucvgprlemm  7605  caucvgprlemopl  7606  caucvgprlemlol  7607  caucvgprlemopu  7608  caucvgprlemupu  7609  caucvgprlemdisj  7611  caucvgprlemloc  7612  caucvgprlemladdfu  7614  caucvgprlem2  7617  caucvgprprlemell  7622  caucvgprprlemelu  7623  caucvgprprlemml  7631  caucvgprprlemmu  7632  caucvgprprlemexbt  7643  caucvgprprlem2  7647  suplocexprlem2b  7651  suplocexprlemlub  7661  sup3exmid  8848  dfuzi  9297  uzval  9464  ixxval  9828  fzval  9942  oddennn  12321  evenennn  12322  znnen  12327  ctiunct  12369  fncld  12698  xmetunirn  12958  limccl  13228  ellimc3apf  13229  subctctexmid  13841