Theorem rabex 4178

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

Syntax hints:   ∈ wcel 2167  {crab 2479  Vcvv 2763

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-sep 4152

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rab 2484  df-v 2765  df-in 3163  df-ss 3170

This theorem is referenced by:  rab2ex  4181  repizf2  4196  undifexmid  4227  exmidexmid  4230  ordtriexmidlem  4556  ordtri2or2exmidlem  4563  onsucelsucexmidlem  4566  regexmid  4572  reg2exmid  4573  reg3exmid  4617  nnregexmid  4658  ssimaex  5625  mptrabex  5793  acexmidlemcase  5920  acexmidlemv  5923  fnpm  6724  ssfiexmid  6946  domfiexmid  6948  inffiexmid  6976  ctssdclemr  7187  nninfex  7196  ctssexmid  7225  exmidonfinlem  7274  exmidaclem  7293  genpelvl  7598  genpelvu  7599  genipdm  7602  ltexprlemell  7684  ltexprlemelu  7685  cauappcvgprlemm  7731  cauappcvgprlemopl  7732  cauappcvgprlemlol  7733  cauappcvgprlemopu  7734  cauappcvgprlemupu  7735  cauappcvgprlemdisj  7737  cauappcvgprlemloc  7738  cauappcvgprlemladdfu  7740  cauappcvgprlemladdfl  7741  cauappcvgprlemladdru  7742  cauappcvgprlemladdrl  7743  cauappcvgprlem1  7745  cauappcvgprlem2  7746  caucvgprlemm  7754  caucvgprlemopl  7755  caucvgprlemlol  7756  caucvgprlemopu  7757  caucvgprlemupu  7758  caucvgprlemdisj  7760  caucvgprlemloc  7761  caucvgprlemladdfu  7763  caucvgprlem2  7766  caucvgprprlemell  7771  caucvgprprlemelu  7772  caucvgprprlemml  7780  caucvgprprlemmu  7781  caucvgprprlemexbt  7792  caucvgprprlem2  7796  suplocexprlem2b  7800  suplocexprlemlub  7810  sup3exmid  9003  dfuzi  9455  uzval  9622  ixxval  9990  fzval  10104  bitsfval  12126  oddennn  12636  evenennn  12637  znnen  12642  ctiunct  12684  rhmex  13791  metuex  14189  expghmap  14241  psrval  14300  fnpsr  14301  fnmpl  14327  fncld  14442  xmetunirn  14702  limccl  15003  ellimc3apf  15004  subctctexmid  15755