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

Theorem rabexg 4180
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 3271 . 2  |-  { x  e.  A  |  ph }  C_  A
2 ssexg 4176 . 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 1696   {crab 2560   _Vcvv 2801    C_ wss 3165
This theorem is referenced by:  rabex  4181  class2set  4194  exse  4373  wdom2d  7310  scottex  7571  tskwe  7599  fin1a2lem12  8053  hashbclem  11406  hashdvds  12859  hashbcval  13065  fctop  16757  cctop  16759  ppttop  16760  epttop  16762  cldval  16776  mretopd  16845  neif  16853  neival  16855  ordtbaslem  16934  ordtbas2  16937  ordtopn1  16940  ordtopn2  16941  ordtrest2lem  16949  cmpsublem  17142  kgenval  17246  qtopval  17402  kqfval  17430  ordthmeolem  17508  elmptrab  17538  fbssfi  17548  fgval  17581  flimval  17674  flimfnfcls  17739  ptcmplem2  17763  ptcmplem3  17764  tsmsfbas  17826  eltsms  17831  blval  17964  minveclem3b  18808  minveclem3  18809  minveclem4  18812  hasheuni  23468  sigaex  23485  sigaval  23486  imambfm  23582  iscvm  23805  cvmsval  23812  ubos  25359  mxlelt  25367  mnlelt2  25369  isinob  25965  issrc  25970  isntr  25976  fnessref  26396  indexa  26515  supex2g  26522  cnfex  27802  stoweidlem26  27878  stoweidlem31  27883  stoweidlem34  27886  stoweidlem35  27887  stoweidlem46  27898  stoweidlem50  27902  stoweidlem57  27909  stoweidlem59  27911  mpt2xopoveq  28201  nbgraop  28274  isuvtx  28301
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator