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

Theorem rabex 4314
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 4313 . 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 1721   {crab 2670   _Vcvv 2916
This theorem is referenced by:  frminex  4522  ssimaex  5747  fnpm  6985  inf3lema  7535  cantnffval  7574  dfac2a  7966  kmlem1  7986  axcc4  8275  axdc3lem2  8287  axdc3lem4  8289  pwfseqlem1  8489  nqex  8756  dfuzi  10316  uzval  10446  ixxval  10880  fzval  11001  bitsfval  12890  sadfval  12919  smufval  12944  phicl2  13112  odzval  13132  prmreclem4  13242  prmreclem5  13243  ismre  13770  fnmre  13771  mrisval  13810  isacs  13831  ismon  13914  isnat  14099  natffn  14101  coafval  14174  ismhm  14695  issubm  14703  gsumvalx  14729  issubg  14899  isnsg  14924  gimfn  15003  isgim  15004  isga  15023  cntzval  15075  odval  15127  odf  15130  odngen  15166  gexval  15167  sylow1lem2  15188  isslw  15197  sylow3lem6  15221  dmdprd  15514  dprdval  15516  ablfac1a  15582  ablfac1b  15583  ablfac1c  15584  ablfac1eu  15586  ablfaclem1  15598  ablfaclem2  15599  ablfaclem3  15600  isirred  15759  issubrg  15823  abvfval  15861  lssset  15965  lmimfn  16057  islmhm  16058  islmim  16089  islbs  16103  rrgval  16302  psrval  16384  gsumbagdiag  16396  psrbas  16398  psrelbas  16399  psraddcl  16402  psrmulfval  16404  psrmulcllem  16406  psrvscaval  16411  psrvscacl  16412  psr0cl  16413  psr0lid  16414  psrnegcl  16415  psrlinv  16416  psrgrp  16417  psrlmod  16420  psr1cl  16421  psrlidm  16422  psrridm  16423  psrdi  16425  psrdir  16426  psrass23  16428  subrgpsr  16437  mvrval  16440  mvrf  16443  mplsubglem  16453  mplvscaval  16466  mplmon  16481  mplcoe1  16483  mplbas2  16486  ltbval  16487  opsrval  16490  opsrtoslem2  16500  mplmon2  16508  evlslem2  16523  psrplusgpropd  16584  psropprmul  16587  ocvval  16849  elocv  16850  isobs  16902  fncld  17041  cnfval  17251  cnpval  17254  iscnp2  17257  1stcfb  17461  kgenf  17526  xkoopn  17574  dfac14  17603  hmeofn  17742  hmeofval  17743  filunirn  17867  alexsubALTlem2  18032  ucnval  18260  iscfilu  18271  ispsmet  18288  ismet  18306  isxmet  18307  xmetunirn  18320  cncfval  18871  ishtpy  18950  isphtpy  18959  om1bas  19009  cfilfval  19170  caufval  19181  iscmet  19190  dyadmax  19443  vitalilem2  19454  vitalilem3  19455  vitalilem4  19456  itg2monolem1  19595  fncpn  19772  elcpn  19773  evlslem3  19888  evlslem1  19889  mdegaddle  19950  mdegvsca  19952  mdegmullem  19954  uc1pval  20015  mon1pval  20017  aannenlem1  20198  aannenlem2  20199  aannenlem3  20200  vmaval  20849  vmaf  20855  sqff1o  20918  musum  20929  0sgmppw  20935  dchrval  20971  dchrbas  20972  lnoval  22206  bloval  22235  hmoval  22264  ubthlem1  22325  ubthlem2  22326  ocval  22735  eigvecval  23352  specval  23354  sigaex  24445  isrnsigaOLD  24448  ismbfm  24555  elunirnmbfm  24556  sitgval  24600  ballotlem8  24747  lgamgulmlem5  24770  lgamgulmlem6  24771  lgamgulm2  24773  lgamcvglem  24777  fncvm  24897  iscvm  24899  snmlval  24971  elgiso  25060  fvray  25979  cnambfre  26154  istotbnd  26368  isbnd  26379  rngohomval  26470  rngoisoval  26483  idlval  26513  pridlval  26533  maxidlval  26539  isnacs  26648  mzpclval  26672  pell1qrval  26799  pell14qrval  26801  pell1234qrval  26803  mapfien2  27126  pwfi2en  27129  islinds  27147  elmnc  27209  itgoval  27234  pmtrfval  27261  psgnfval  27291  issdrg  27373  idomodle  27380  idomsubgmo  27382  hashgcdeq  27385  stoweidlem34  27650  bnj110  28935  lshpset  29461  lflset  29542  pats  29768  llnset  29987  lplnset  30011  lvolset  30054  isline  30221  pmapval  30239  paddval  30280  lhpset  30477  ldilset  30591  ltrnset  30600  dilsetN  30635  trnsetN  30638  diafval  31514  diaval  31515  diafn  31517  dicfval  31658  lpolsetN  31965  lcdvadd  32080  lcdsca  32082  lcdvs  32086  mapdval  32111  mapd1o  32131  mapdunirnN  32133
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator