Theorem rabex 3958

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

Syntax hints:   ∈ wcel 1436  {crab 2359  Vcvv 2615

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 3932

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 2617  df-in 2994  df-ss 3001

This theorem is referenced by:  repizf2  3972  undifexmid  4002  exmidexmid  4005  ordtriexmidlem  4309  ordtri2or2exmidlem  4315  onsucelsucexmidlem  4318  regexmid  4324  reg2exmid  4325  reg3exmid  4368  nnregexmid  4407  ssimaex  5328  acexmidlemcase  5608  acexmidlemv  5611  fnpm  6365  ssfiexmid  6544  domfiexmid  6546  inffiexmid  6574  genpelvl  7015  genpelvu  7016  genipdm  7019  ltexprlemell  7101  ltexprlemelu  7102  cauappcvgprlemm  7148  cauappcvgprlemopl  7149  cauappcvgprlemlol  7150  cauappcvgprlemopu  7151  cauappcvgprlemupu  7152  cauappcvgprlemdisj  7154  cauappcvgprlemloc  7155  cauappcvgprlemladdfu  7157  cauappcvgprlemladdfl  7158  cauappcvgprlemladdru  7159  cauappcvgprlemladdrl  7160  cauappcvgprlem1  7162  cauappcvgprlem2  7163  caucvgprlemm  7171  caucvgprlemopl  7172  caucvgprlemlol  7173  caucvgprlemopu  7174  caucvgprlemupu  7175  caucvgprlemdisj  7177  caucvgprlemloc  7178  caucvgprlemladdfu  7180  caucvgprlem2  7183  caucvgprprlemell  7188  caucvgprprlemelu  7189  caucvgprprlemml  7197  caucvgprprlemmu  7198  caucvgprprlemexbt  7209  caucvgprprlem2  7213  dfuzi  8789  uzval  8953  ixxval  9246  fzval  9358  oddennn  11080  evenennn  11081  znnen  11086  nninfex  11339