Theorem rabexg 4281

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 3333	. 2 |- { x e. A | ph } C_ A
2		ssexg 4274	. 2 |- ( ( { x e. A | ph } C_ A /\ A e. V ) -> { x e. A | ph } e. _V )
3	1, 2	mpan 428	1 |- ( A e. V -> { x e. A | ph } e. _V )

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   {crab 2532   _Vcvv 2821   C_ wss 3220

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:  rabex  4282  rabexd  4283  exmidsssnc  4342  exse  4483  frind  4499  elfvmptrab1  5804  elovmporab  6292  elovmporab1w  6293  suppval  6481  mpoxopoveq  6516  diffitest  7197  supex2g  7379  cc4f  7641  omctfn  13391  ismhm  13826  mhmex  13827  issubm  13837  issubg  14034  subgex  14037  isnsg  14063  isrim0  14576  issubrng  14615  issubrg  14637  rrgval  14678  lssex  14799  lsssetm  14801  psrval  15160  psrplusgg  15191  psraddcl  15193  epttop  15333  cldval  15342  neif  15384  neival  15386  cnfval  15437  cnovex  15439  cnpval  15441  hmeofn  15545  hmeofvalg  15546  ispsmet  15566  ismet  15587  isxmet  15588  blvalps  15631  blval  15632  cncfval  15815  clwwlkg  16856  clwwlknon  16892