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

Theorem rabexg 4463
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 3458 . 2  |-  { x  e.  A  |  ph }  C_  A
2 ssexg 4459 . 2  |-  ( ( { x  e.  A  |  ph }  C_  A  /\  A  e.  V
)  ->  { x  e.  A  |  ph }  e.  _V )
31, 2mpan 670 1  |-  ( A  e.  V  ->  { x  e.  A  |  ph }  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   {crab 2740   _Vcvv 2993    C_ wss 3349
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4434
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rab 2745  df-v 2995  df-in 3356  df-ss 3363
This theorem is referenced by:  rabex  4464  rabexd  4465  class2set  4480  exse  4705  suppval  6713  mpt2xopoveq  6757  wdom2d  7816  scottex  8113  tskwe  8141  fin1a2lem12  8601  hashbclem  12226  hashdvds  13871  hashbcval  14084  psrass1lem  17469  psrdi  17501  psrdir  17502  psrcom  17503  fctop  18630  cctop  18632  ppttop  18633  epttop  18635  cldval  18649  mretopd  18718  neif  18726  neival  18728  neiptoptop  18757  neiptopnei  18758  ordtbaslem  18814  ordtbas2  18817  ordtopn1  18820  ordtopn2  18821  ordtrest2lem  18829  cmpsublem  19024  kgenval  19130  qtopval  19290  kqfval  19318  ordthmeolem  19396  elmptrab  19422  fbssfi  19432  fgval  19465  flimval  19558  flimfnfcls  19623  ptcmplem2  19647  ptcmplem3  19648  tsmsfbas  19720  eltsms  19725  utopval  19829  blvalps  19982  blval  19983  minveclem3b  20937  minveclem3  20938  minveclem4  20941  fiusgraedgfi  23342  nbgraop  23357  cusgraexilem1  23396  isuvtx  23418  vdgrf  23590  vdgrun  23593  vdusgraval  23599  hashnbgravdg  23603  usgravd0nedg  23604  ordtrest2NEWlem  26374  hasheuni  26556  sigaval  26575  braew  26680  imambfm  26699  iscvm  27170  cvmsval  27177  fnessref  28591  indexa  28653  supex2g  28657  cnfex  29776  stoweidlem26  29847  stoweidlem31  29852  stoweidlem34  29855  stoweidlem46  29867  stoweidlem59  29880  elfvmptrab1  30180  elovmpt2rab  30184  elovmpt2rab1  30185  ovmpt3rabdm  30188  elovmpt3rab1  30189  wrd2f1tovbij  30281  wwlk  30341  wwlkn  30342  wwlkextbij  30391  wwlkexthasheq  30392  2wlkonot  30410  2spthonot  30411  2wlksot  30412  2spthsot  30413  clwwlk  30455  clwwlkn  30456  wrdnfi  30502  rusgranumwlkl1lem1  30584  vdn0frgrav2  30642  vdgn0frgrav2  30643  vdn1frgrav2  30644  vdgn1frgrav2  30645  frgrawopreglem1  30663  usg2spot2nb  30684  usgreg2spot  30686  2spotmdisj  30687  usgreghash2spot  30688  numclwwlkovf  30700  lcoop  30942  cnstpmat  31061
  Copyright terms: Public domain W3C validator