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

Theorem rabex 4181
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 4180 . 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 1696   {crab 2560   _Vcvv 2801
This theorem is referenced by:  frminex  4389  ssimaex  5600  fnpm  6796  inf3lema  7341  cantnffval  7380  dfac2a  7772  kmlem1  7792  axcc4  8081  axdc3lem2  8093  axdc3lem4  8095  pwfseqlem1  8296  nqex  8563  dfuzi  10118  uzval  10248  ixxval  10680  fzval  10800  bitsfval  12630  sadfval  12659  smufval  12684  phicl2  12852  odzval  12872  prmreclem4  12982  prmreclem5  12983  ismre  13508  fnmre  13509  mrisval  13548  isacs  13569  ismon  13652  isnat  13837  natffn  13839  coafval  13912  ismhm  14433  issubm  14441  gsumvalx  14467  issubg  14637  isnsg  14662  gimfn  14741  isgim  14742  isga  14761  cntzval  14813  odval  14865  odf  14868  odngen  14904  gexval  14905  sylow1lem2  14926  isslw  14935  sylow3lem6  14959  dmdprd  15252  dprdval  15254  ablfac1a  15320  ablfac1b  15321  ablfac1c  15322  ablfac1eu  15324  ablfaclem1  15336  ablfaclem2  15337  ablfaclem3  15338  isirred  15497  issubrg  15561  abvfval  15599  lssset  15707  lmimfn  15799  islmhm  15800  islmim  15831  islbs  15845  rrgval  16044  psrval  16126  gsumbagdiag  16138  psrbas  16140  psrelbas  16141  psraddcl  16144  psrmulfval  16146  psrmulcllem  16148  psrvscaval  16153  psrvscacl  16154  psr0cl  16155  psr0lid  16156  psrnegcl  16157  psrlinv  16158  psrgrp  16159  psrlmod  16162  psr1cl  16163  psrlidm  16164  psrridm  16165  psrdi  16167  psrdir  16168  psrass23  16170  subrgpsr  16179  mvrval  16182  mvrf  16185  mplsubglem  16195  mplvscaval  16208  mplmon  16223  mplcoe1  16225  mplbas2  16228  ltbval  16229  opsrval  16232  opsrtoslem2  16242  mplmon2  16250  evlslem2  16265  psrplusgpropd  16329  psropprmul  16332  ocvval  16583  elocv  16584  isobs  16636  fncld  16775  cnfval  16979  cnpval  16982  iscnp2  16985  1stcfb  17187  kgenf  17252  xkoopn  17300  dfac14  17328  hmeofn  17464  hmeofval  17465  filunirn  17593  alexsubALTlem2  17758  ismet  17904  isxmet  17905  xmetunirn  17918  cncfval  18408  ishtpy  18486  isphtpy  18495  om1bas  18545  cfilfval  18706  caufval  18717  iscmet  18726  dyadmax  18969  vitalilem2  18980  vitalilem3  18981  vitalilem4  18982  itg2monolem1  19121  fncpn  19298  elcpn  19299  evlslem3  19414  evlslem1  19415  mdegaddle  19476  mdegvsca  19478  mdegmullem  19480  uc1pval  19541  mon1pval  19543  aannenlem1  19724  aannenlem2  19725  aannenlem3  19726  vmaval  20367  vmaf  20373  sqff1o  20436  musum  20447  0sgmppw  20453  dchrval  20489  dchrbas  20490  lnoval  21346  bloval  21375  hmoval  21404  ubthlem1  21465  ubthlem2  21466  ocval  21875  eigvecval  22492  specval  22494  ballotlem2  23063  ballotlem8  23111  ballotth  23112  isrnsigaOLD  23488  ismbfm  23572  elunirnmbfm  23573  fncvm  23803  iscvm  23805  snmlval  23929  elgiso  24018  fvray  24836  isorhom  25314  idlvalNEW  25548  ishomb  25891  ismona  25912  isepia  25922  isiso  25928  cinvlem2  25932  isfuna  25937  propsrc  25971  islimcat  25979  isnword  26089  isconcl1b  26200  sgplpte21  26235  sgplpte22  26241  isray2  26256  isray  26257  istotbnd  26596  isbnd  26607  rngohomval  26698  rngoisoval  26711  idlval  26741  pridlval  26761  maxidlval  26767  isnacs  26882  mzpclval  26906  pell1qrval  27034  pell14qrval  27036  pell1234qrval  27038  mapfien2  27361  pwfi2en  27364  islinds  27382  elmnc  27444  itgoval  27469  pmtrfval  27496  psgnfval  27526  issdrg  27608  idomodle  27615  idomsubgmo  27617  hashgcdeq  27620  stoweidlem34  27886  bnj110  29206  lshpset  29790  lflset  29871  pats  30097  llnset  30316  lplnset  30340  lvolset  30383  isline  30550  pmapval  30568  paddval  30609  lhpset  30806  ldilset  30920  ltrnset  30929  dilsetN  30964  trnsetN  30967  diafval  31843  diaval  31844  diafn  31846  dicfval  31987  lpolsetN  32294  lcdvadd  32409  lcdsca  32411  lcdvs  32415  mapdval  32440  mapd1o  32460  mapdunirnN  32462
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator