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

Theorem rabexg 4570
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 3546 . 2  |-  { x  e.  A  |  ph }  C_  A
2 ssexg 4566 . 2  |-  ( ( { x  e.  A  |  ph }  C_  A  /\  A  e.  V
)  ->  { x  e.  A  |  ph }  e.  _V )
31, 2mpan 674 1  |-  ( A  e.  V  ->  { x  e.  A  |  ph }  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1868   {crab 2779   _Vcvv 3081    C_ wss 3436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-rab 2784  df-v 3083  df-in 3443  df-ss 3450
This theorem is referenced by:  rabex  4571  rabexd  4572  class2set  4587  exse  4813  elfvmptrab1  5982  elovmpt2rab  6525  elovmpt2rab1  6526  ovmpt3rabdm  6536  elovmpt3rab1  6537  suppval  6923  mpt2xopoveq  6969  wdom2d  8097  scottex  8357  tskwe  8385  fin1a2lem12  8841  hashbclem  12612  wrdnfi  12690  wrd2f1tovbij  13021  hashdvds  14708  hashbcval  14939  brric  17957  psrass1lem  18586  psrcom  18618  dmatval  19501  cpmat  19717  fctop  20003  cctop  20005  ppttop  20006  epttop  20008  cldval  20022  neif  20100  neival  20102  neiptoptop  20131  neiptopnei  20132  ordtbaslem  20188  ordtbas2  20191  ordtopn1  20194  ordtopn2  20195  ordtrest2lem  20203  cmpsublem  20398  kgenval  20534  qtopval  20694  kqfval  20722  ordthmeolem  20800  elmptrab  20826  fbssfi  20836  fgval  20869  flimval  20962  flimfnfcls  21027  ptcmplem2  21052  ptcmplem3  21053  tsmsfbas  21126  eltsms  21131  utopval  21231  blvalps  21384  blval  21385  minveclem3b  22354  minveclem3  22355  minveclem4  22358  minveclem3bOLD  22366  minveclem3OLD  22367  minveclem4OLD  22370  fiusgraedgfi  25118  nbgraop  25134  isuvtx  25199  wwlk  25392  wwlkn  25393  wwlkextbij  25444  wwlkexthasheq  25445  clwwlk  25477  clwwlkn  25478  2wlkonot  25576  2spthonot  25577  2wlksot  25578  2spthsot  25579  vdgrf  25609  vdgrun  25612  vdusgraval  25618  hashnbgravdg  25624  usgravd0nedg  25629  rusgranumwwlkl1  25657  vdn0frgrav2  25734  vdgn0frgrav2  25735  vdn1frgrav2  25736  vdgn1frgrav2  25737  frgrawopreglem1  25755  usg2spot2nb  25776  usgreg2spot  25778  2spotmdisj  25779  usgreghash2spot  25780  rabfodom  28124  ordtrest2NEWlem  28721  hasheuni  28899  sigaval  28925  ldgenpisyslem1  28978  ddemeas  29052  braew  29058  imambfm  29077  carsgval  29128  iscvm  29975  cvmsval  29982  fwddifval  30919  fnessref  31003  indexa  31971  supex2g  31975  cnfex  37207  stoweidlem26  37703  stoweidlem31  37709  stoweidlem34  37712  stoweidlem46  37724  stoweidlem59  37737  caragenval  38090  dmatALTbas  39382  lcoop  39392
  Copyright terms: Public domain W3C validator