Theorem rabex 4173

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

Syntax hints:   ∈ wcel 2164  {crab 2476  Vcvv 2760

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-sep 4147

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rab 2481  df-v 2762  df-in 3159  df-ss 3166

This theorem is referenced by:  rab2ex  4176  repizf2  4191  undifexmid  4222  exmidexmid  4225  ordtriexmidlem  4551  ordtri2or2exmidlem  4558  onsucelsucexmidlem  4561  regexmid  4567  reg2exmid  4568  reg3exmid  4612  nnregexmid  4653  ssimaex  5618  mptrabex  5786  acexmidlemcase  5913  acexmidlemv  5916  fnpm  6710  ssfiexmid  6932  domfiexmid  6934  inffiexmid  6962  ctssdclemr  7171  nninfex  7180  ctssexmid  7209  exmidonfinlem  7253  exmidaclem  7268  genpelvl  7572  genpelvu  7573  genipdm  7576  ltexprlemell  7658  ltexprlemelu  7659  cauappcvgprlemm  7705  cauappcvgprlemopl  7706  cauappcvgprlemlol  7707  cauappcvgprlemopu  7708  cauappcvgprlemupu  7709  cauappcvgprlemdisj  7711  cauappcvgprlemloc  7712  cauappcvgprlemladdfu  7714  cauappcvgprlemladdfl  7715  cauappcvgprlemladdru  7716  cauappcvgprlemladdrl  7717  cauappcvgprlem1  7719  cauappcvgprlem2  7720  caucvgprlemm  7728  caucvgprlemopl  7729  caucvgprlemlol  7730  caucvgprlemopu  7731  caucvgprlemupu  7732  caucvgprlemdisj  7734  caucvgprlemloc  7735  caucvgprlemladdfu  7737  caucvgprlem2  7740  caucvgprprlemell  7745  caucvgprprlemelu  7746  caucvgprprlemml  7754  caucvgprprlemmu  7755  caucvgprprlemexbt  7766  caucvgprprlem2  7770  suplocexprlem2b  7774  suplocexprlemlub  7784  sup3exmid  8976  dfuzi  9427  uzval  9594  ixxval  9962  fzval  10076  oddennn  12549  evenennn  12550  znnen  12555  ctiunct  12597  rhmex  13653  expghmap  14095  psrval  14152  fnpsr  14153  fncld  14266  xmetunirn  14526  limccl  14813  ellimc3apf  14814  subctctexmid  15491