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

Theorem rabex 4297
Description: Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 19-Jul-1996.)
Hypothesis
Ref Expression
rabex.1  |-  A  e. 
_V
Assertion
Ref Expression
rabex  |-  { x  e.  A  |  ph }  e.  _V
Distinct variable group:    x, A
Allowed substitution hint:    ph( x)

Proof of Theorem rabex
StepHypRef Expression
1 rabex.1 . 2  |-  A  e. 
_V
2 rabexg 4296 . 2  |-  ( A  e.  _V  ->  { x  e.  A  |  ph }  e.  _V )
31, 2ax-mp 8 1  |-  { x  e.  A  |  ph }  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1717   {crab 2655   _Vcvv 2901
This theorem is referenced by:  frminex  4505  ssimaex  5729  fnpm  6964  inf3lema  7514  cantnffval  7553  dfac2a  7945  kmlem1  7965  axcc4  8254  axdc3lem2  8266  axdc3lem4  8268  pwfseqlem1  8468  nqex  8735  dfuzi  10294  uzval  10424  ixxval  10858  fzval  10979  bitsfval  12864  sadfval  12893  smufval  12918  phicl2  13086  odzval  13106  prmreclem4  13216  prmreclem5  13217  ismre  13744  fnmre  13745  mrisval  13784  isacs  13805  ismon  13888  isnat  14073  natffn  14075  coafval  14148  ismhm  14669  issubm  14677  gsumvalx  14703  issubg  14873  isnsg  14898  gimfn  14977  isgim  14978  isga  14997  cntzval  15049  odval  15101  odf  15104  odngen  15140  gexval  15141  sylow1lem2  15162  isslw  15171  sylow3lem6  15195  dmdprd  15488  dprdval  15490  ablfac1a  15556  ablfac1b  15557  ablfac1c  15558  ablfac1eu  15560  ablfaclem1  15572  ablfaclem2  15573  ablfaclem3  15574  isirred  15733  issubrg  15797  abvfval  15835  lssset  15939  lmimfn  16031  islmhm  16032  islmim  16063  islbs  16077  rrgval  16276  psrval  16358  gsumbagdiag  16370  psrbas  16372  psrelbas  16373  psraddcl  16376  psrmulfval  16378  psrmulcllem  16380  psrvscaval  16385  psrvscacl  16386  psr0cl  16387  psr0lid  16388  psrnegcl  16389  psrlinv  16390  psrgrp  16391  psrlmod  16394  psr1cl  16395  psrlidm  16396  psrridm  16397  psrdi  16399  psrdir  16400  psrass23  16402  subrgpsr  16411  mvrval  16414  mvrf  16417  mplsubglem  16427  mplvscaval  16440  mplmon  16455  mplcoe1  16457  mplbas2  16460  ltbval  16461  opsrval  16464  opsrtoslem2  16474  mplmon2  16482  evlslem2  16497  psrplusgpropd  16558  psropprmul  16561  ocvval  16819  elocv  16820  isobs  16872  fncld  17011  cnfval  17221  cnpval  17224  iscnp2  17227  1stcfb  17431  kgenf  17496  xkoopn  17544  dfac14  17573  hmeofn  17712  hmeofval  17713  filunirn  17837  alexsubALTlem2  18002  ucnval  18230  iscfilu  18241  ismet  18264  isxmet  18265  xmetunirn  18278  cncfval  18791  ishtpy  18870  isphtpy  18879  om1bas  18929  cfilfval  19090  caufval  19101  iscmet  19110  dyadmax  19359  vitalilem2  19370  vitalilem3  19371  vitalilem4  19372  itg2monolem1  19511  fncpn  19688  elcpn  19689  evlslem3  19804  evlslem1  19805  mdegaddle  19866  mdegvsca  19868  mdegmullem  19870  uc1pval  19931  mon1pval  19933  aannenlem1  20114  aannenlem2  20115  aannenlem3  20116  vmaval  20765  vmaf  20771  sqff1o  20834  musum  20845  0sgmppw  20851  dchrval  20887  dchrbas  20888  lnoval  22103  bloval  22132  hmoval  22161  ubthlem1  22222  ubthlem2  22223  ocval  22632  eigvecval  23249  specval  23251  sigaex  24290  isrnsigaOLD  24293  ismbfm  24398  elunirnmbfm  24399  ballotlem8  24575  lgamgulmlem5  24598  lgamgulmlem6  24599  lgamgulm2  24601  lgamcvglem  24605  fncvm  24725  iscvm  24727  snmlval  24799  elgiso  24888  fvray  25791  istotbnd  26171  isbnd  26182  rngohomval  26273  rngoisoval  26286  idlval  26316  pridlval  26336  maxidlval  26342  isnacs  26451  mzpclval  26475  pell1qrval  26602  pell14qrval  26604  pell1234qrval  26606  mapfien2  26929  pwfi2en  26932  islinds  26950  elmnc  27012  itgoval  27037  pmtrfval  27064  psgnfval  27094  issdrg  27176  idomodle  27183  idomsubgmo  27185  hashgcdeq  27188  stoweidlem34  27453  bnj110  28569  lshpset  29095  lflset  29176  pats  29402  llnset  29621  lplnset  29645  lvolset  29688  isline  29855  pmapval  29873  paddval  29914  lhpset  30111  ldilset  30225  ltrnset  30234  dilsetN  30269  trnsetN  30272  diafval  31148  diaval  31149  diafn  31151  dicfval  31292  lpolsetN  31599  lcdvadd  31714  lcdsca  31716  lcdvs  31720  mapdval  31745  mapd1o  31765  mapdunirnN  31767
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370  ax-sep 4273
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-rab 2660  df-v 2903  df-in 3272  df-ss 3279
  Copyright terms: Public domain W3C validator