Theorem rabex 4232

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

Syntax hints:   ∈ wcel 2200  {crab 2512  Vcvv 2800

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4205

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rab 2517  df-v 2802  df-in 3204  df-ss 3211

This theorem is referenced by:  rab2ex  4235  repizf2  4250  undifexmid  4281  exmidexmid  4284  ordtriexmidlem  4615  ordtri2or2exmidlem  4622  onsucelsucexmidlem  4625  regexmid  4631  reg2exmid  4632  reg3exmid  4676  nnregexmid  4717  ssimaex  5703  mptrabex  5877  acexmidlemcase  6008  acexmidlemv  6011  fnpm  6820  ssfiexmid  7058  domfiexmid  7060  inffiexmid  7091  ctssdclemr  7302  nninfex  7311  ctssexmid  7340  exmidonfinlem  7394  exmidaclem  7413  genpelvl  7722  genpelvu  7723  genipdm  7726  ltexprlemell  7808  ltexprlemelu  7809  cauappcvgprlemm  7855  cauappcvgprlemopl  7856  cauappcvgprlemlol  7857  cauappcvgprlemopu  7858  cauappcvgprlemupu  7859  cauappcvgprlemdisj  7861  cauappcvgprlemloc  7862  cauappcvgprlemladdfu  7864  cauappcvgprlemladdfl  7865  cauappcvgprlemladdru  7866  cauappcvgprlemladdrl  7867  cauappcvgprlem1  7869  cauappcvgprlem2  7870  caucvgprlemm  7878  caucvgprlemopl  7879  caucvgprlemlol  7880  caucvgprlemopu  7881  caucvgprlemupu  7882  caucvgprlemdisj  7884  caucvgprlemloc  7885  caucvgprlemladdfu  7887  caucvgprlem2  7890  caucvgprprlemell  7895  caucvgprprlemelu  7896  caucvgprprlemml  7904  caucvgprprlemmu  7905  caucvgprprlemexbt  7916  caucvgprprlem2  7920  suplocexprlem2b  7924  suplocexprlemlub  7934  sup3exmid  9127  dfuzi  9580  uzval  9747  ixxval  10121  fzval  10235  bitsfval  12493  oddennn  13003  evenennn  13004  znnen  13009  ctiunct  13051  rhmex  14161  metuex  14559  expghmap  14611  psrval  14670  fnpsr  14671  fnmpl  14697  fncld  14812  xmetunirn  15072  limccl  15373  ellimc3apf  15374  clwwlknon  16224  clwwlk0on0  16226  subctctexmid  16537