Theorem rabexg 4107

Description: Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 23-Oct-1999.)

Assertion

Ref	Expression
rabexg	|- ( A e. V -> { x e. A | ph } e. _V )

Distinct variable group:   x, A

Allowed substitution hints:   ph( x)   V( x)

Proof of Theorem rabexg

Step	Hyp	Ref	Expression
1		ssrab2 3213	. 2 |- { x e. A | ph } C_ A
2		ssexg 4103	. 2 |- ( ( { x e. A | ph } C_ A /\ A e. V ) -> { x e. A | ph } e. _V )
3	1, 2	mpan 421	1 |- ( A e. V -> { x e. A | ph } e. _V )

Syntax hints:   -> wi 4   e. wcel 2128   {crab 2439   _Vcvv 2712   C_ wss 3102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139  ax-sep 4082

This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-rab 2444  df-v 2714  df-in 3108  df-ss 3115

This theorem is referenced by:  rabex  4108  exmidsssnc  4164  exse  4296  frind  4312  elfvmptrab1  5562  mpoxopoveq  6187  diffitest  6832  supex2g  6977  cc4f  7189  omctfn  12172  epttop  12490  cldval  12499  neif  12541  neival  12543  cnfval  12594  cnovex  12596  cnpval  12598  hmeofn  12702  hmeofvalg  12703  ispsmet  12723  ismet  12744  isxmet  12745  blvalps  12788  blval  12789  cncfval  12959