Theorem rabex 4280

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

This proof depends on syntax axioms:   ∈ wcel 2209  {crab 2532  Vcvv 2821

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-sep 4249

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rab 2537  df-v 2823  df-in 3226  df-ss 3233

This theorem is used by:  rab2ex  4283  repizf2  4299  undifexmid  4330  exmidexmid  4333  ordtriexmidlem  4666  ordtri2or2exmidlem  4673  onsucelsucexmidlem  4676  regexmid  4682  reg2exmid  4683  reg3exmid  4727  nnregexmid  4768  ssimaex  5764  mptrabex  5946  acexmidlemcase  6080  acexmidlemv  6083  fnpm  6930  ssfiexmid  7178  ssfiexmidt  7180  domfiexmid  7182  inffiexmid  7213  ctssdclemr  7452  nninfex  7461  ctssexmid  7490  exmidonfinlem  7545  exmidaclem  7564  genpelvl  7879  genpelvu  7880  genipdm  7883  ltexprlemell  7965  ltexprlemelu  7966  cauappcvgprlemm  8012  cauappcvgprlemopl  8013  cauappcvgprlemlol  8014  cauappcvgprlemopu  8015  cauappcvgprlemupu  8016  cauappcvgprlemdisj  8018  cauappcvgprlemloc  8019  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  cauappcvgprlem1  8026  cauappcvgprlem2  8027  caucvgprlemm  8035  caucvgprlemopl  8036  caucvgprlemlol  8037  caucvgprlemopu  8038  caucvgprlemupu  8039  caucvgprlemdisj  8041  caucvgprlemloc  8042  caucvgprlemladdfu  8044  caucvgprlem2  8047  caucvgprprlemell  8052  caucvgprprlemelu  8053  caucvgprprlemml  8061  caucvgprprlemmu  8062  caucvgprprlemexbt  8073  caucvgprprlem2  8077  suplocexprlem2b  8081  suplocexprlemlub  8091  sup3exmid  9287  dfuzi  9756  uzval  9923  ixxval  10298  fzval  10413  bitsfval  12709  ballotfilem8  13280  oddennn  13283  evenennn  13284  znnen  13289  ctiunct  13331  rhmex  14464  metuex  14892  expghmap  14942  psrval  15050  fnpsr  15051  fnmpl  15084  fncld  15199  xmetunirn  15459  limccl  15760  ellimc3apf  15761  clwwlknon  16670  clwwlk0on0  16672  subctctexmid  17030  wexmiddiffilem  17043  wexmiddifxy  17046