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  7453  nninfex  7462  ctssexmid  7491  exmidonfinlem  7546  exmidaclem  7565  genpelvl  7880  genpelvu  7881  genipdm  7884  ltexprlemell  7966  ltexprlemelu  7967  cauappcvgprlemm  8013  cauappcvgprlemopl  8014  cauappcvgprlemlol  8015  cauappcvgprlemopu  8016  cauappcvgprlemupu  8017  cauappcvgprlemdisj  8019  cauappcvgprlemloc  8020  cauappcvgprlemladdfu  8022  cauappcvgprlemladdfl  8023  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  cauappcvgprlem1  8027  cauappcvgprlem2  8028  caucvgprlemm  8036  caucvgprlemopl  8037  caucvgprlemlol  8038  caucvgprlemopu  8039  caucvgprlemupu  8040  caucvgprlemdisj  8042  caucvgprlemloc  8043  caucvgprlemladdfu  8045  caucvgprlem2  8048  caucvgprprlemell  8053  caucvgprprlemelu  8054  caucvgprprlemml  8062  caucvgprprlemmu  8063  caucvgprprlemexbt  8074  caucvgprprlem2  8078  suplocexprlem2b  8082  suplocexprlemlub  8092  sup3exmid  9290  dfuzi  9761  uzval  9933  ixxval  10309  fzval  10424  bitsfval  12728  ballotfilem8  13332  oddennn  13335  evenennn  13336  znnen  13341  ctiunct  13383  rhmex  14548  metuex  14976  expghmap  15026  psrval  15134  fnpsr  15135  fnmpl  15175  fncld  15290  xmetunirn  15550  limccl  15851  ellimc3apf  15852  clwwlknon  16836  clwwlk0on0  16838  subctctexmid  17196  wexmiddiffilem  17209  wexmiddifxy  17212