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

Theorem rabexg 4597
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 3585 . 2  |-  { x  e.  A  |  ph }  C_  A
2 ssexg 4593 . 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 1767   {crab 2818   _Vcvv 3113    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-in 3483  df-ss 3490
This theorem is referenced by:  rabex  4598  rabexd  4599  class2set  4614  exse  4843  elfvmptrab1  5970  elovmpt2rab  6505  elovmpt2rab1  6506  ovmpt3rabdm  6519  elovmpt3rab1  6520  suppval  6903  mpt2xopoveq  6947  wdom2d  8006  scottex  8303  tskwe  8331  fin1a2lem12  8791  hashbclem  12467  wrdnfi  12539  wrd2f1tovbij  12861  hashdvds  14164  hashbcval  14379  brric  17193  psrass1lem  17828  psrdi  17860  psrdir  17861  psrcom  17863  dmatval  18789  cpmat  19005  fctop  19299  cctop  19301  ppttop  19302  epttop  19304  cldval  19318  mretopd  19387  neif  19395  neival  19397  neiptoptop  19426  neiptopnei  19427  ordtbaslem  19483  ordtbas2  19486  ordtopn1  19489  ordtopn2  19490  ordtrest2lem  19498  cmpsublem  19693  kgenval  19799  qtopval  19959  kqfval  19987  ordthmeolem  20065  elmptrab  20091  fbssfi  20101  fgval  20134  flimval  20227  flimfnfcls  20292  ptcmplem2  20316  ptcmplem3  20317  tsmsfbas  20389  eltsms  20394  utopval  20498  blvalps  20651  blval  20652  minveclem3b  21606  minveclem3  21607  minveclem4  21610  fiusgraedgfi  24111  nbgraop  24127  cusgraexilem1  24170  isuvtx  24192  wwlk  24385  wwlkn  24386  wwlkextbij  24437  wwlkexthasheq  24438  clwwlk  24470  clwwlkn  24471  2wlkonot  24569  2spthonot  24570  2wlksot  24571  2spthsot  24572  vdgrf  24602  vdgrun  24605  vdusgraval  24611  hashnbgravdg  24617  usgravd0nedg  24622  rusgranumwwlkl1  24650  vdn0frgrav2  24728  vdgn0frgrav2  24729  vdn1frgrav2  24730  vdgn1frgrav2  24731  frgrawopreglem1  24749  usg2spot2nb  24770  usgreg2spot  24772  2spotmdisj  24773  usgreghash2spot  24774  numclwwlkovf  24786  ordtrest2NEWlem  27568  hasheuni  27759  sigaval  27778  braew  27882  imambfm  27901  iscvm  28372  cvmsval  28379  fnessref  29793  indexa  29855  supex2g  29859  cnfex  31009  stoweidlem26  31354  stoweidlem31  31359  stoweidlem34  31362  stoweidlem46  31374  stoweidlem59  31387  dmatALTbas  32101  lcoop  32111
  Copyright terms: Public domain W3C validator