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

Theorem rabexg 4345
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 3420 . 2  |-  { x  e.  A  |  ph }  C_  A
2 ssexg 4341 . 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 1725   {crab 2701   _Vcvv 2948    C_ wss 3312
This theorem is referenced by:  rabex  4346  class2set  4359  exse  4538  mpt2xopoveq  6462  wdom2d  7540  scottex  7801  tskwe  7829  fin1a2lem12  8283  hashbclem  11693  hashdvds  13156  hashbcval  13362  fctop  17060  cctop  17062  ppttop  17063  epttop  17065  cldval  17079  mretopd  17148  neif  17156  neival  17158  neiptoptop  17187  neiptopnei  17188  ordtbaslem  17244  ordtbas2  17247  ordtopn1  17250  ordtopn2  17251  ordtrest2lem  17259  cmpsublem  17454  kgenval  17559  qtopval  17719  kqfval  17747  ordthmeolem  17825  elmptrab  17851  fbssfi  17861  fgval  17894  flimval  17987  flimfnfcls  18052  ptcmplem2  18076  ptcmplem3  18077  tsmsfbas  18149  eltsms  18154  utopval  18254  blvalps  18407  blval  18408  minveclem3b  19321  minveclem3  19322  minveclem4  19325  fiusgraedgfi  21413  nbgraop  21428  cusgraexilem1  21467  isuvtx  21489  vdgrf  21661  vdgrun  21664  vdusgraval  21670  hashnbgravdg  21674  usgravd0nedg  21675  hasheuni  24467  sigaval  24485  braew  24585  imambfm  24604  iscvm  24938  cvmsval  24945  fnessref  26364  indexa  26426  supex2g  26430  cnfex  27666  stoweidlem26  27742  stoweidlem31  27747  stoweidlem34  27750  stoweidlem35  27751  stoweidlem46  27762  stoweidlem50  27766  stoweidlem57  27773  stoweidlem59  27775  2wlkonot  28285  2spthonot  28286  2wlksot  28287  2spthsot  28288  vdn0frgrav2  28351  vdgn0frgrav2  28352  vdn1frgrav2  28353  vdgn1frgrav2  28354  frgrawopreglem1  28370  usg2spot2nb  28391  usgreg2spot  28393  2spotmdisj  28394  usgreghash2spot  28395
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-v 2950  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator