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

Theorem rabex 4455
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 4454 . 2  |-  ( A  e.  _V  ->  { x  e.  A  |  ph }  e.  _V )
31, 2ax-mp 5 1  |-  { x  e.  A  |  ph }  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756   {crab 2731   _Vcvv 2984
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4425
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rab 2736  df-v 2986  df-in 3347  df-ss 3354
This theorem is referenced by:  rab2ex  4458  frminex  4712  ssimaex  5768  mptrabex  5961  fnpm  7234  mapfien2  7670  inf3lema  7842  cantnffval  7881  dfac2a  8311  kmlem1  8331  axcc4  8620  axdc3lem2  8632  axdc3lem4  8634  pwfseqlem1  8837  nqex  9104  dfuzi  10744  uzval  10875  ixxval  11320  fzval  11451  bitsfval  13631  sadfval  13660  smufval  13685  phicl2  13855  odzval  13875  prmreclem4  13992  prmreclem5  13993  ismre  14540  fnmre  14541  mrisval  14580  isacs  14601  ismon  14684  isnat  14869  natffn  14871  coafval  14944  ismhm  15478  issubm  15487  gsumvalx  15514  issubg  15693  isnsg  15722  gimfn  15801  isgim  15802  isga  15821  cntzval  15851  pmtrfval  15968  psgnfval  16018  odval  16049  odngen  16088  gexval  16089  sylow1lem2  16110  isslw  16119  sylow3lem6  16143  dmdprd  16492  dprdval  16497  dprdvalOLD  16499  ablfac1a  16582  ablfac1b  16583  ablfac1c  16584  ablfac1eu  16586  ablfaclem1  16598  ablfaclem2  16599  ablfaclem3  16600  isirred  16803  isrim0  16825  issubrg  16877  abvfval  16915  lssset  17027  lmimfn  17119  islmhm  17120  islmim  17155  islbs  17169  rrgval  17370  psrval  17441  gsumbagdiag  17458  psrass1lem  17459  psrbas  17460  psrbasOLD  17461  psrelbas  17462  psraddcl  17466  psrmulfval  17468  psrmulcllem  17470  psrvscaval  17475  psrvscacl  17476  psr0cl  17477  psr0lid  17478  psrnegcl  17479  psrlinv  17480  psrgrp  17481  psrlmod  17484  psr1cl  17485  psrlidmOLD  17487  psrridmOLD  17489  psrdi  17491  psrdir  17492  psrcom  17493  subrgpsr  17503  mvrval  17506  mvrf  17509  mplsubglemOLD  17524  mplsubrg  17531  mplvscaval  17539  mplmonmul  17555  mplbas2  17563  mplbas2OLD  17564  ltbval  17565  opsrval  17568  opsrtoslem2  17578  mplmon2  17587  psrplusgpropd  17702  psropprmul  17705  ocvval  18104  elocv  18105  isobs  18157  islinds  18250  fncld  18638  cnfval  18849  cnpval  18852  iscnp2  18855  1stcfb  19061  kgenf  19126  xkoopn  19174  dfac14  19203  hmeofn  19342  hmeofval  19343  filunirn  19467  alexsubALTlem2  19632  ucnval  19864  iscfilu  19875  ispsmet  19892  ismet  19910  isxmet  19911  xmetunirn  19924  cncfval  20476  ishtpy  20556  isphtpy  20565  om1bas  20615  cfilfval  20787  caufval  20798  iscmet  20807  rrxmet  20919  dyadmax  21090  vitalilem2  21101  vitalilem3  21102  vitalilem4  21103  itg2monolem1  21240  fncpn  21419  elcpn  21420  mdegleb  21547  mdegldg  21549  mdeg0  21553  mdegaddle  21557  mdegvsca  21559  mdegmullem  21561  uc1pval  21623  mon1pval  21625  aannenlem1  21806  aannenlem2  21807  aannenlem3  21808  vmaval  22463  sqff1o  22532  musum  22543  0sgmppw  22549  dchrval  22585  dchrbas  22586  tglnfn  22993  tglnunirn  22994  tglngval  22997  israg  23103  ttgitvval  23140  ebtwntg  23240  lnoval  24164  bloval  24193  hmoval  24222  ubthlem1  24283  ubthlem2  24284  ocval  24695  eigvecval  25312  specval  25314  ordtconlem1  26366  sigaex  26564  isrnsigaOLD  26567  ddemeas  26664  ismbfm  26679  elunirnmbfm  26680  sitgval  26730  eulerpartlemt  26766  eulerpartgbij  26767  eulerpart  26777  ballotlem8  26931  lgamgulmlem5  27031  lgamgulmlem6  27032  lgamgulm2  27034  lgamcvglem  27038  fncvm  27158  iscvm  27160  snmlval  27232  elgiso  27327  fvray  28184  fin2solem  28427  fin2so  28428  cnambfre  28452  istotbnd  28680  isbnd  28691  rngohomval  28782  rngoisoval  28795  idlval  28825  pridlval  28845  maxidlval  28851  isnacs  29052  mzpclval  29073  pell1qrval  29199  pell14qrval  29201  pell1234qrval  29203  mapfien2OLD  29461  pwfi2en  29464  elmnc  29505  itgoval  29530  issdrg  29566  idomodle  29573  idomsubgmo  29575  hashgcdeq  29578  stoweidlem34  29841  wlknwwlknbij2  30358  wlkiswwlkbij2  30365  wlknwwlknvbij  30384  clwwlkbij  30473  clwwlkvbij  30475  clwlksizeeq  30537  rusgranumwlklem1  30579  rusgranumwlklem3  30581  rusgranumwlklem4  30582  rusgranumwwlkg  30589  numclwwlkovg  30692  numclwwlkovq  30704  numclwwlkqhash  30705  numclwwlkovh  30706  bnj110  31863  lshpset  32635  lflset  32716  pats  32942  llnset  33161  lplnset  33185  lvolset  33228  isline  33395  pmapval  33413  paddval  33454  lhpset  33651  ldilset  33765  ltrnset  33774  dilsetN  33809  trnsetN  33812  diafval  34688  diaval  34689  diafn  34691  dicfval  34832  lpolsetN  35139  lcdvadd  35254  lcdsca  35256  lcdvs  35260  mapdval  35285  mapd1o  35305  mapdunirnN  35307
  Copyright terms: Public domain W3C validator