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

Theorem rabex 4346
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 4345 . 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 1725   {crab 2701   _Vcvv 2948
This theorem is referenced by:  frminex  4554  ssimaex  5780  fnpm  7018  inf3lema  7571  cantnffval  7610  dfac2a  8002  kmlem1  8022  axcc4  8311  axdc3lem2  8323  axdc3lem4  8325  pwfseqlem1  8525  nqex  8792  dfuzi  10352  uzval  10482  ixxval  10916  fzval  11037  bitsfval  12927  sadfval  12956  smufval  12981  phicl2  13149  odzval  13169  prmreclem4  13279  prmreclem5  13280  ismre  13807  fnmre  13808  mrisval  13847  isacs  13868  ismon  13951  isnat  14136  natffn  14138  coafval  14211  ismhm  14732  issubm  14740  gsumvalx  14766  issubg  14936  isnsg  14961  gimfn  15040  isgim  15041  isga  15060  cntzval  15112  odval  15164  odf  15167  odngen  15203  gexval  15204  sylow1lem2  15225  isslw  15234  sylow3lem6  15258  dmdprd  15551  dprdval  15553  ablfac1a  15619  ablfac1b  15620  ablfac1c  15621  ablfac1eu  15623  ablfaclem1  15635  ablfaclem2  15636  ablfaclem3  15637  isirred  15796  issubrg  15860  abvfval  15898  lssset  16002  lmimfn  16094  islmhm  16095  islmim  16126  islbs  16140  rrgval  16339  psrval  16421  gsumbagdiag  16433  psrbas  16435  psrelbas  16436  psraddcl  16439  psrmulfval  16441  psrmulcllem  16443  psrvscaval  16448  psrvscacl  16449  psr0cl  16450  psr0lid  16451  psrnegcl  16452  psrlinv  16453  psrgrp  16454  psrlmod  16457  psr1cl  16458  psrlidm  16459  psrridm  16460  psrdi  16462  psrdir  16463  psrass23  16465  subrgpsr  16474  mvrval  16477  mvrf  16480  mplsubglem  16490  mplvscaval  16503  mplmon  16518  mplcoe1  16520  mplbas2  16523  ltbval  16524  opsrval  16527  opsrtoslem2  16537  mplmon2  16545  evlslem2  16560  psrplusgpropd  16621  psropprmul  16624  ocvval  16886  elocv  16887  isobs  16939  fncld  17078  cnfval  17289  cnpval  17292  iscnp2  17295  1stcfb  17500  kgenf  17565  xkoopn  17613  dfac14  17642  hmeofn  17781  hmeofval  17782  filunirn  17906  alexsubALTlem2  18071  ucnval  18299  iscfilu  18310  ispsmet  18327  ismet  18345  isxmet  18346  xmetunirn  18359  cncfval  18910  ishtpy  18989  isphtpy  18998  om1bas  19048  cfilfval  19209  caufval  19220  iscmet  19229  dyadmax  19482  vitalilem2  19493  vitalilem3  19494  vitalilem4  19495  itg2monolem1  19634  fncpn  19811  elcpn  19812  evlslem3  19927  evlslem1  19928  mdegaddle  19989  mdegvsca  19991  mdegmullem  19993  uc1pval  20054  mon1pval  20056  aannenlem1  20237  aannenlem2  20238  aannenlem3  20239  vmaval  20888  vmaf  20894  sqff1o  20957  musum  20968  0sgmppw  20974  dchrval  21010  dchrbas  21011  lnoval  22245  bloval  22274  hmoval  22303  ubthlem1  22364  ubthlem2  22365  ocval  22774  eigvecval  23391  specval  23393  sigaex  24484  isrnsigaOLD  24487  ismbfm  24594  elunirnmbfm  24595  sitgval  24639  ballotlem8  24786  lgamgulmlem5  24809  lgamgulmlem6  24810  lgamgulm2  24812  lgamcvglem  24816  fncvm  24936  iscvm  24938  snmlval  25010  elgiso  25099  fvray  26067  cnambfre  26245  istotbnd  26469  isbnd  26480  rngohomval  26571  rngoisoval  26584  idlval  26614  pridlval  26634  maxidlval  26640  isnacs  26749  mzpclval  26773  pell1qrval  26900  pell14qrval  26902  pell1234qrval  26904  mapfien2  27226  pwfi2en  27229  islinds  27247  elmnc  27309  itgoval  27334  pmtrfval  27361  psgnfval  27391  issdrg  27473  idomodle  27480  idomsubgmo  27482  hashgcdeq  27485  stoweidlem34  27750  bnj110  29166  lshpset  29713  lflset  29794  pats  30020  llnset  30239  lplnset  30263  lvolset  30306  isline  30473  pmapval  30491  paddval  30532  lhpset  30729  ldilset  30843  ltrnset  30852  dilsetN  30887  trnsetN  30890  diafval  31766  diaval  31767  diafn  31769  dicfval  31910  lpolsetN  32217  lcdvadd  32332  lcdsca  32334  lcdvs  32338  mapdval  32363  mapd1o  32383  mapdunirnN  32385
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-v 2950  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator