MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rabexg Unicode version

Theorem rabexg 4164
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
StepHypRef Expression
1 ssrab2 3258 . 2  |-  { x  e.  A  |  ph }  C_  A
2 ssexg 4160 . 2  |-  ( ( { x  e.  A  |  ph }  C_  A  /\  A  e.  V
)  ->  { x  e.  A  |  ph }  e.  _V )
31, 2mpan 651 1  |-  ( A  e.  V  ->  { x  e.  A  |  ph }  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   {crab 2547   _Vcvv 2788    C_ wss 3152
This theorem is referenced by:  rabex  4165  class2set  4178  exse  4357  wdom2d  7294  scottex  7555  tskwe  7583  fin1a2lem12  8037  hashbclem  11390  hashdvds  12843  hashbcval  13049  fctop  16741  cctop  16743  ppttop  16744  epttop  16746  cldval  16760  mretopd  16829  neif  16837  neival  16839  ordtbaslem  16918  ordtbas2  16921  ordtopn1  16924  ordtopn2  16925  ordtrest2lem  16933  cmpsublem  17126  kgenval  17230  qtopval  17386  kqfval  17414  ordthmeolem  17492  elmptrab  17522  fbssfi  17532  fgval  17565  flimval  17658  flimfnfcls  17723  ptcmplem2  17747  ptcmplem3  17748  tsmsfbas  17810  eltsms  17815  blval  17948  minveclem3b  18792  minveclem3  18793  minveclem4  18796  hasheuni  23453  sigaex  23470  sigaval  23471  imambfm  23567  iscvm  23790  cvmsval  23797  ubos  25256  mxlelt  25264  mnlelt2  25266  isinob  25862  issrc  25867  isntr  25873  fnessref  26293  indexa  26412  supex2g  26419  cnfex  27699  stoweidlem26  27775  stoweidlem31  27780  stoweidlem34  27783  stoweidlem35  27784  stoweidlem46  27795  stoweidlem50  27799  stoweidlem57  27806  stoweidlem59  27808  mpt2xopoveq  28085  nbgraop  28140  isuvtx  28160
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator