Theorem rabex 3951

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

Syntax hints:   ∈ wcel 1436  {crab 2359  Vcvv 2614

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3925

This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-rab 2364  df-v 2616  df-in 2992  df-ss 2999

This theorem is referenced by:  repizf2  3965  undifexmid  3995  exmidexmid  3998  ordtriexmidlem  4302  ordtri2or2exmidlem  4308  onsucelsucexmidlem  4311  regexmid  4317  reg2exmid  4318  reg3exmid  4361  nnregexmid  4400  ssimaex  5313  acexmidlemcase  5589  acexmidlemv  5592  fnpm  6346  ssfiexmid  6525  domfiexmid  6527  inffiexmid  6552  genpelvl  6992  genpelvu  6993  genipdm  6996  ltexprlemell  7078  ltexprlemelu  7079  cauappcvgprlemm  7125  cauappcvgprlemopl  7126  cauappcvgprlemlol  7127  cauappcvgprlemopu  7128  cauappcvgprlemupu  7129  cauappcvgprlemdisj  7131  cauappcvgprlemloc  7132  cauappcvgprlemladdfu  7134  cauappcvgprlemladdfl  7135  cauappcvgprlemladdru  7136  cauappcvgprlemladdrl  7137  cauappcvgprlem1  7139  cauappcvgprlem2  7140  caucvgprlemm  7148  caucvgprlemopl  7149  caucvgprlemlol  7150  caucvgprlemopu  7151  caucvgprlemupu  7152  caucvgprlemdisj  7154  caucvgprlemloc  7155  caucvgprlemladdfu  7157  caucvgprlem2  7160  caucvgprprlemell  7165  caucvgprprlemelu  7166  caucvgprprlemml  7174  caucvgprprlemmu  7175  caucvgprprlemexbt  7186  caucvgprprlem2  7190  dfuzi  8766  uzval  8930  ixxval  9223  fzval  9335  oddennn  10999  evenennn  11000  znnen  11005  nninfex  11257