MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rabexg Structured version   Visualization 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 3526 . 2  |-  { x  e.  A  |  ph }  C_  A
2 ssexg 4565 . 2  |-  ( ( { x  e.  A  |  ph }  C_  A  /\  A  e.  V
)  ->  { x  e.  A  |  ph }  e.  _V )
31, 2mpan 681 1  |-  ( A  e.  V  ->  { x  e.  A  |  ph }  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1898   {crab 2753   _Vcvv 3057    C_ wss 3416
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rab 2758  df-v 3059  df-in 3423  df-ss 3430
This theorem is referenced by:  rabex  4571  rabexd  4572  class2set  4587  exse  4820  elfvmptrab1  5998  elovmpt2rab  6547  elovmpt2rab1  6548  ovmpt3rabdm  6558  elovmpt3rab1  6559  suppval  6948  mpt2xopoveq  6997  wdom2d  8126  scottex  8387  tskwe  8415  fin1a2lem12  8872  hashbclem  12654  wrdnfi  12742  wrd2f1tovbij  13090  hashdvds  14778  hashbcval  15009  brric  18027  psrass1lem  18656  psrcom  18688  dmatval  19572  cpmat  19788  fctop  20074  cctop  20076  ppttop  20077  epttop  20079  cldval  20093  neif  20171  neival  20173  neiptoptop  20202  neiptopnei  20203  ordtbaslem  20259  ordtbas2  20262  ordtopn1  20265  ordtopn2  20266  ordtrest2lem  20274  cmpsublem  20469  kgenval  20605  qtopval  20765  kqfval  20793  ordthmeolem  20871  elmptrab  20897  fbssfi  20907  fgval  20940  flimval  21033  flimfnfcls  21098  ptcmplem2  21123  ptcmplem3  21124  tsmsfbas  21197  eltsms  21202  utopval  21302  blvalps  21455  blval  21456  minveclem3b  22425  minveclem3  22426  minveclem4  22429  minveclem3bOLD  22437  minveclem3OLD  22438  minveclem4OLD  22441  fiusgraedgfi  25191  nbgraop  25207  isuvtx  25272  wwlk  25465  wwlkn  25466  wwlkextbij  25517  wwlkexthasheq  25518  clwwlk  25550  clwwlkn  25551  2wlkonot  25649  2spthonot  25650  2wlksot  25651  2spthsot  25652  vdgrf  25682  vdgrun  25685  vdusgraval  25691  hashnbgravdg  25697  usgravd0nedg  25702  rusgranumwwlkl1  25730  vdn0frgrav2  25807  vdgn0frgrav2  25808  vdn1frgrav2  25809  vdgn1frgrav2  25810  frgrawopreglem1  25828  usg2spot2nb  25849  usgreg2spot  25851  2spotmdisj  25852  usgreghash2spot  25853  rabfodom  28196  ordtrest2NEWlem  28779  hasheuni  28957  sigaval  28983  ldgenpisyslem1  29036  ddemeas  29109  braew  29115  imambfm  29134  carsgval  29185  iscvm  30032  cvmsval  30039  fwddifval  30979  fnessref  31063  indexa  32106  supex2g  32110  cnfex  37390  stoweidlem26  37987  stoweidlem31  37993  stoweidlem34  37996  stoweidlem46  38008  stoweidlem59  38021  salexct  38294  caragenval  38422  fusgredgfi  39537  nbgrval  39552  cusgrsize  39661  dmatALTbas  40563  lcoop  40573
  Copyright terms: Public domain W3C validator