Theorem rabexg 4188

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 4184	. 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 4163

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  4189  rabexd  4190  exmidsssnc  4248  exse  4384  frind  4400  elfvmptrab1  5676  elovmporab  6148  elovmporab1w  6149  mpoxopoveq  6328  diffitest  6986  supex2g  7137  cc4f  7383  omctfn  12847  ismhm  13326  mhmex  13327  issubm  13337  issubg  13542  subgex  13545  isnsg  13571  isrim0  13956  issubrng  13994  issubrg  14016  rrgval  14057  lssex  14149  lsssetm  14151  psrval  14461  psrplusgg  14473  psraddcl  14475  epttop  14595  cldval  14604  neif  14646  neival  14648  cnfval  14699  cnovex  14701  cnpval  14703  hmeofn  14807  hmeofvalg  14808  ispsmet  14828  ismet  14849  isxmet  14850  blvalps  14893  blval  14894  cncfval  15077