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

Theorem rabexg 4430
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 3425 . 2  |-  { x  e.  A  |  ph }  C_  A
2 ssexg 4426 . 2  |-  ( ( { x  e.  A  |  ph }  C_  A  /\  A  e.  V
)  ->  { x  e.  A  |  ph }  e.  _V )
31, 2mpan 663 1  |-  ( A  e.  V  ->  { x  e.  A  |  ph }  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1755   {crab 2709   _Vcvv 2962    C_ wss 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714  df-v 2964  df-in 3323  df-ss 3330
This theorem is referenced by:  rabex  4431  rabexd  4432  class2set  4447  exse  4671  suppval  6681  mpt2xopoveq  6725  wdom2d  7783  scottex  8080  tskwe  8108  fin1a2lem12  8568  hashbclem  12188  hashdvds  13832  hashbcval  14045  psrass1lem  17380  psrdi  17412  psrdir  17413  psrcom  17414  fctop  18449  cctop  18451  ppttop  18452  epttop  18454  cldval  18468  mretopd  18537  neif  18545  neival  18547  neiptoptop  18576  neiptopnei  18577  ordtbaslem  18633  ordtbas2  18636  ordtopn1  18639  ordtopn2  18640  ordtrest2lem  18648  cmpsublem  18843  kgenval  18949  qtopval  19109  kqfval  19137  ordthmeolem  19215  elmptrab  19241  fbssfi  19251  fgval  19284  flimval  19377  flimfnfcls  19442  ptcmplem2  19466  ptcmplem3  19467  tsmsfbas  19539  eltsms  19544  utopval  19648  blvalps  19801  blval  19802  minveclem3b  20756  minveclem3  20757  minveclem4  20760  fiusgraedgfi  23142  nbgraop  23157  cusgraexilem1  23196  isuvtx  23218  vdgrf  23390  vdgrun  23393  vdusgraval  23399  hashnbgravdg  23403  usgravd0nedg  23404  ordtrest2NEWlem  26205  hasheuni  26387  sigaval  26406  braew  26511  imambfm  26530  iscvm  26995  cvmsval  27002  fnessref  28406  indexa  28468  supex2g  28472  cnfex  29592  stoweidlem26  29664  stoweidlem31  29669  stoweidlem34  29672  stoweidlem35  29673  stoweidlem46  29684  stoweidlem50  29688  stoweidlem57  29695  stoweidlem59  29697  elfvmptrab1  29997  elovmpt2rab  30001  elovmpt2rab1  30002  ovmpt3rabdm  30005  elovmpt3rab1  30006  wrd2f1tovbij  30098  wwlk  30158  wwlkn  30159  wwlkextbij  30208  wwlkexthasheq  30209  2wlkonot  30227  2spthonot  30228  2wlksot  30229  2spthsot  30230  clwwlk  30272  clwwlkn  30273  wrdnfi  30319  rusgranumwlkl1lem1  30401  vdn0frgrav2  30459  vdgn0frgrav2  30460  vdn1frgrav2  30461  vdgn1frgrav2  30462  frgrawopreglem1  30480  usg2spot2nb  30501  usgreg2spot  30503  2spotmdisj  30504  usgreghash2spot  30505  numclwwlkovf  30517  lcoop  30651
  Copyright terms: Public domain W3C validator