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

Theorem rabexg 4583
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 3567 . 2  |-  { x  e.  A  |  ph }  C_  A
2 ssexg 4579 . 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 1802   {crab 2795   _Vcvv 3093    C_ wss 3458
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-rab 2800  df-v 3095  df-in 3465  df-ss 3472
This theorem is referenced by:  rabex  4584  rabexd  4585  class2set  4600  exse  4829  elfvmptrab1  5957  elovmpt2rab  6502  elovmpt2rab1  6503  ovmpt3rabdm  6516  elovmpt3rab1  6517  suppval  6901  mpt2xopoveq  6945  wdom2d  8004  scottex  8301  tskwe  8329  fin1a2lem12  8789  hashbclem  12475  wrdnfi  12548  wrd2f1tovbij  12872  hashdvds  14177  hashbcval  14392  brric  17261  psrass1lem  17897  psrcom  17932  dmatval  18861  cpmat  19077  fctop  19371  cctop  19373  ppttop  19374  epttop  19376  cldval  19390  neif  19467  neival  19469  neiptoptop  19498  neiptopnei  19499  ordtbaslem  19555  ordtbas2  19558  ordtopn1  19561  ordtopn2  19562  ordtrest2lem  19570  cmpsublem  19765  kgenval  19902  qtopval  20062  kqfval  20090  ordthmeolem  20168  elmptrab  20194  fbssfi  20204  fgval  20237  flimval  20330  flimfnfcls  20395  ptcmplem2  20419  ptcmplem3  20420  tsmsfbas  20492  eltsms  20497  utopval  20601  blvalps  20754  blval  20755  minveclem3b  21709  minveclem3  21710  minveclem4  21713  fiusgraedgfi  24272  nbgraop  24288  isuvtx  24353  wwlk  24546  wwlkn  24547  wwlkextbij  24598  wwlkexthasheq  24599  clwwlk  24631  clwwlkn  24632  2wlkonot  24730  2spthonot  24731  2wlksot  24732  2spthsot  24733  vdgrf  24763  vdgrun  24766  vdusgraval  24772  hashnbgravdg  24778  usgravd0nedg  24783  rusgranumwwlkl1  24811  vdn0frgrav2  24888  vdgn0frgrav2  24889  vdn1frgrav2  24890  vdgn1frgrav2  24891  frgrawopreglem1  24909  usg2spot2nb  24930  usgreg2spot  24932  2spotmdisj  24933  usgreghash2spot  24934  rabfodom  27269  ordtrest2NEWlem  27770  hasheuni  27957  sigaval  27976  ddemeas  28074  braew  28080  imambfm  28099  iscvm  28570  cvmsval  28577  fnessref  30143  indexa  30192  supex2g  30196  cnfex  31350  stoweidlem26  31693  stoweidlem31  31698  stoweidlem34  31701  stoweidlem46  31713  stoweidlem59  31726  dmatALTbas  32712  lcoop  32722
  Copyright terms: Public domain W3C validator