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  6935  ssfiexmid  7184  ssfiexmidt  7186  domfiexmid  7188  inffiexmid  7219  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  9766  uzval  9938  ixxval  10314  fzval  10429  bitsfval  12733  ballotfilem8  13337  oddennn  13340  evenennn  13341  znnen  13346  ctiunct  13388  rhmex  14572  metuex  15000  expghmap  15050  psrval  15160  fnpsr  15161  fnmpl  15225  fncld  15341  xmetunirn  15601  limccl  15902  ellimc3apf  15903  clwwlknon  16892  clwwlk0on0  16894  subctctexmid  17252  wexmiddiffilem  17265  wexmiddifxy  17268