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

Theorem rabexg 4313
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 3388 . 2  |-  { x  e.  A  |  ph }  C_  A
2 ssexg 4309 . 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 1721   {crab 2670   _Vcvv 2916    C_ wss 3280
This theorem is referenced by:  rabex  4314  class2set  4327  exse  4506  mpt2xopoveq  6429  wdom2d  7504  scottex  7765  tskwe  7793  fin1a2lem12  8247  hashbclem  11656  hashdvds  13119  hashbcval  13325  fctop  17023  cctop  17025  ppttop  17026  epttop  17028  cldval  17042  mretopd  17111  neif  17119  neival  17121  neiptoptop  17150  neiptopnei  17151  ordtbaslem  17206  ordtbas2  17209  ordtopn1  17212  ordtopn2  17213  ordtrest2lem  17221  cmpsublem  17416  kgenval  17520  qtopval  17680  kqfval  17708  ordthmeolem  17786  elmptrab  17812  fbssfi  17822  fgval  17855  flimval  17948  flimfnfcls  18013  ptcmplem2  18037  ptcmplem3  18038  tsmsfbas  18110  eltsms  18115  utopval  18215  blvalps  18368  blval  18369  minveclem3b  19282  minveclem3  19283  minveclem4  19286  fiusgraedgfi  21374  nbgraop  21389  cusgraexilem1  21428  isuvtx  21450  vdgrf  21622  vdgrun  21625  vdusgraval  21631  hashnbgravdg  21635  usgravd0nedg  21636  hasheuni  24428  sigaval  24446  braew  24546  imambfm  24565  iscvm  24899  cvmsval  24906  fnessref  26263  indexa  26325  supex2g  26329  cnfex  27566  stoweidlem26  27642  stoweidlem31  27647  stoweidlem34  27650  stoweidlem35  27651  stoweidlem46  27662  stoweidlem50  27666  stoweidlem57  27673  stoweidlem59  27675  2wlkonot  28062  2spthonot  28063  2wlksot  28064  2spthsot  28065  vdn0frgrav2  28128  vdgn0frgrav2  28129  vdn1frgrav2  28130  vdgn1frgrav2  28131  frgrawopreglem1  28147  usg2spot2nb  28168  usgreg2spot  28170  2spotmdisj  28171  usgreghash2spot  28172
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator