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

Theorem rabex 4165
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 4164 . 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 1684   {crab 2547   _Vcvv 2788
This theorem is referenced by:  frminex  4373  ssimaex  5584  fnpm  6780  inf3lema  7325  cantnffval  7364  dfac2a  7756  kmlem1  7776  axcc4  8065  axdc3lem2  8077  axdc3lem4  8079  pwfseqlem1  8280  nqex  8547  dfuzi  10102  uzval  10232  ixxval  10664  fzval  10784  bitsfval  12614  sadfval  12643  smufval  12668  phicl2  12836  odzval  12856  prmreclem4  12966  prmreclem5  12967  ismre  13492  fnmre  13493  mrisval  13532  isacs  13553  ismon  13636  isnat  13821  natffn  13823  coafval  13896  ismhm  14417  issubm  14425  gsumvalx  14451  issubg  14621  isnsg  14646  gimfn  14725  isgim  14726  isga  14745  cntzval  14797  odval  14849  odf  14852  odngen  14888  gexval  14889  sylow1lem2  14910  isslw  14919  sylow3lem6  14943  dmdprd  15236  dprdval  15238  ablfac1a  15304  ablfac1b  15305  ablfac1c  15306  ablfac1eu  15308  ablfaclem1  15320  ablfaclem2  15321  ablfaclem3  15322  isirred  15481  issubrg  15545  abvfval  15583  lssset  15691  lmimfn  15783  islmhm  15784  islmim  15815  islbs  15829  rrgval  16028  psrval  16110  gsumbagdiag  16122  psrbas  16124  psrelbas  16125  psraddcl  16128  psrmulfval  16130  psrmulcllem  16132  psrvscaval  16137  psrvscacl  16138  psr0cl  16139  psr0lid  16140  psrnegcl  16141  psrlinv  16142  psrgrp  16143  psrlmod  16146  psr1cl  16147  psrlidm  16148  psrridm  16149  psrdi  16151  psrdir  16152  psrass23  16154  subrgpsr  16163  mvrval  16166  mvrf  16169  mplsubglem  16179  mplvscaval  16192  mplmon  16207  mplcoe1  16209  mplbas2  16212  ltbval  16213  opsrval  16216  opsrtoslem2  16226  mplmon2  16234  evlslem2  16249  psrplusgpropd  16313  psropprmul  16316  ocvval  16567  elocv  16568  isobs  16620  fncld  16759  cnfval  16963  cnpval  16966  iscnp2  16969  1stcfb  17171  kgenf  17236  xkoopn  17284  dfac14  17312  hmeofn  17448  hmeofval  17449  filunirn  17577  alexsubALTlem2  17742  ismet  17888  isxmet  17889  xmetunirn  17902  cncfval  18392  ishtpy  18470  isphtpy  18479  om1bas  18529  cfilfval  18690  caufval  18701  iscmet  18710  dyadmax  18953  vitalilem2  18964  vitalilem3  18965  vitalilem4  18966  itg2monolem1  19105  fncpn  19282  elcpn  19283  evlslem3  19398  evlslem1  19399  mdegaddle  19460  mdegvsca  19462  mdegmullem  19464  uc1pval  19525  mon1pval  19527  aannenlem1  19708  aannenlem2  19709  aannenlem3  19710  vmaval  20351  vmaf  20357  sqff1o  20420  musum  20431  0sgmppw  20437  dchrval  20473  dchrbas  20474  lnoval  21330  bloval  21359  hmoval  21388  ubthlem1  21449  ubthlem2  21450  ocval  21859  eigvecval  22476  specval  22478  ballotlem2  23047  ballotlem8  23095  ballotth  23096  isrnsigaOLD  23473  ismbfm  23557  elunirnmbfm  23558  fncvm  23788  iscvm  23790  snmlval  23914  elgiso  24003  fvray  24764  isorhom  25211  idlvalNEW  25445  ishomb  25788  ismona  25809  isepia  25819  isiso  25825  cinvlem2  25829  isfuna  25834  propsrc  25868  islimcat  25876  isnword  25986  isconcl1b  26097  sgplpte21  26132  sgplpte22  26138  isray2  26153  isray  26154  istotbnd  26493  isbnd  26504  rngohomval  26595  rngoisoval  26608  idlval  26638  pridlval  26658  maxidlval  26664  isnacs  26779  mzpclval  26803  pell1qrval  26931  pell14qrval  26933  pell1234qrval  26935  mapfien2  27258  pwfi2en  27261  islinds  27279  elmnc  27341  itgoval  27366  pmtrfval  27393  psgnfval  27423  issdrg  27505  idomodle  27512  idomsubgmo  27514  hashgcdeq  27517  stoweidlem34  27783  bnj110  28890  lshpset  29168  lflset  29249  pats  29475  llnset  29694  lplnset  29718  lvolset  29761  isline  29928  pmapval  29946  paddval  29987  lhpset  30184  ldilset  30298  ltrnset  30307  dilsetN  30342  trnsetN  30345  diafval  31221  diaval  31222  diafn  31224  dicfval  31365  lpolsetN  31672  lcdvadd  31787  lcdsca  31789  lcdvs  31793  mapdval  31818  mapd1o  31838  mapdunirnN  31840
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator