Theorem rabex 4282

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 4281	. 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 4251

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  4285  repizf2  4301  undifexmid  4332  exmidexmid  4335  ordtriexmidlem  4668  ordtri2or2exmidlem  4675  onsucelsucexmidlem  4678  regexmid  4684  reg2exmid  4685  reg3exmid  4729  nnregexmid  4770  ssimaex  5767  mptrabex  5949  acexmidlemcase  6083  acexmidlemv  6086  fnpm  6934  ssfiexmid  7182  ssfiexmidt  7184  domfiexmid  7186  inffiexmid  7217  ctssdclemr  7458  nninfex  7467  ctssexmid  7496  exmidonfinlem  7551  exmidaclem  7570  genpelvl  7885  genpelvu  7886  genipdm  7889  ltexprlemell  7971  ltexprlemelu  7972  cauappcvgprlemm  8018  cauappcvgprlemopl  8019  cauappcvgprlemlol  8020  cauappcvgprlemopu  8021  cauappcvgprlemupu  8022  cauappcvgprlemdisj  8024  cauappcvgprlemloc  8025  cauappcvgprlemladdfu  8027  cauappcvgprlemladdfl  8028  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  cauappcvgprlem1  8032  cauappcvgprlem2  8033  caucvgprlemm  8041  caucvgprlemopl  8042  caucvgprlemlol  8043  caucvgprlemopu  8044  caucvgprlemupu  8045  caucvgprlemdisj  8047  caucvgprlemloc  8048  caucvgprlemladdfu  8050  caucvgprlem2  8053  caucvgprprlemell  8058  caucvgprprlemelu  8059  caucvgprprlemml  8067  caucvgprprlemmu  8068  caucvgprprlemexbt  8079  caucvgprprlem2  8083  suplocexprlem2b  8087  suplocexprlemlub  8097  sup3exmid  9295  dfuzi  9767  uzval  9939  ixxval  10315  fzval  10430  bitsfval  12734  ballotfilem8  13338  oddennn  13341  evenennn  13342  znnen  13347  ctiunct  13389  rhmex  14573  metuex  15001  expghmap  15051  psrval  15159  fnpsr  15160  fnmpl  15209  fncld  15324  xmetunirn  15584  limccl  15885  ellimc3apf  15886  clwwlknon  16875  clwwlk0on0  16877  subctctexmid  17235  wexmiddiffilem  17248  wexmiddifxy  17251