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

Theorem rabexg 4295
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 3372 . 2  |-  { x  e.  A  |  ph }  C_  A
2 ssexg 4291 . 2  |-  ( ( { x  e.  A  |  ph }  C_  A  /\  A  e.  V
)  ->  { x  e.  A  |  ph }  e.  _V )
31, 2mpan 652 1  |-  ( A  e.  V  ->  { x  e.  A  |  ph }  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717   {crab 2654   _Vcvv 2900    C_ wss 3264
This theorem is referenced by:  rabex  4296  class2set  4309  exse  4488  mpt2xopoveq  6407  wdom2d  7482  scottex  7743  tskwe  7771  fin1a2lem12  8225  hashbclem  11629  hashdvds  13092  hashbcval  13298  fctop  16992  cctop  16994  ppttop  16995  epttop  16997  cldval  17011  mretopd  17080  neif  17088  neival  17090  neiptoptop  17119  neiptopnei  17120  ordtbaslem  17175  ordtbas2  17178  ordtopn1  17181  ordtopn2  17182  ordtrest2lem  17190  cmpsublem  17385  kgenval  17489  qtopval  17649  kqfval  17677  ordthmeolem  17755  elmptrab  17781  fbssfi  17791  fgval  17824  flimval  17917  flimfnfcls  17982  ptcmplem2  18006  ptcmplem3  18007  tsmsfbas  18079  eltsms  18084  utopval  18184  blval  18323  minveclem3b  19197  minveclem3  19198  minveclem4  19201  fiusgraedgfi  21288  nbgraop  21303  cusgraexilem1  21342  isuvtx  21364  vdgrf  21518  vdgrun  21521  vdusgraval  21527  hashnbgravdg  21531  usgravd0nedg  21532  hasheuni  24272  sigaval  24290  braew  24388  imambfm  24407  iscvm  24726  cvmsval  24733  fnessref  26065  indexa  26127  supex2g  26131  cnfex  27368  stoweidlem26  27444  stoweidlem31  27449  stoweidlem34  27452  stoweidlem35  27453  stoweidlem46  27464  stoweidlem50  27468  stoweidlem57  27475  stoweidlem59  27477  vdn0frgrav2  27778  vdgn0frgrav2  27779  vdn1frgrav2  27780  vdgn1frgrav2  27781  frgrawopreglem1  27797
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369  ax-sep 4272
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-rab 2659  df-v 2902  df-in 3271  df-ss 3278
  Copyright terms: Public domain W3C validator