Theorem rabexg 4187

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

Syntax hints:   -> wi 4   e. wcel 2176   {crab 2488   _Vcvv 2772   C_ wss 3166

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-sep 4162

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rab 2493  df-v 2774  df-in 3172  df-ss 3179

This theorem is referenced by:  rabex  4188  rabexd  4189  exmidsssnc  4247  exse  4383  frind  4399  elfvmptrab1  5674  elovmporab  6146  elovmporab1w  6147  mpoxopoveq  6326  diffitest  6984  supex2g  7135  cc4f  7381  omctfn  12814  ismhm  13293  mhmex  13294  issubm  13304  issubg  13509  subgex  13512  isnsg  13538  isrim0  13923  issubrng  13961  issubrg  13983  rrgval  14024  lssex  14116  lsssetm  14118  psrval  14428  psrplusgg  14440  psraddcl  14442  epttop  14562  cldval  14571  neif  14613  neival  14615  cnfval  14666  cnovex  14668  cnpval  14670  hmeofn  14774  hmeofvalg  14775  ispsmet  14795  ismet  14816  isxmet  14817  blvalps  14860  blval  14861  cncfval  15044