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

Theorem rabex 4440
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 4439 . 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 1761   {crab 2717   _Vcvv 2970
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-rab 2722  df-v 2972  df-in 3332  df-ss 3339
This theorem is referenced by:  rab2ex  4443  frminex  4696  ssimaex  5753  mptrabex  5946  fnpm  7218  mapfien2  7654  inf3lema  7826  cantnffval  7865  dfac2a  8295  kmlem1  8315  axcc4  8604  axdc3lem2  8616  axdc3lem4  8618  pwfseqlem1  8821  nqex  9088  dfuzi  10728  uzval  10859  ixxval  11304  fzval  11435  bitsfval  13615  sadfval  13644  smufval  13669  phicl2  13839  odzval  13859  prmreclem4  13976  prmreclem5  13977  ismre  14524  fnmre  14525  mrisval  14564  isacs  14585  ismon  14668  isnat  14853  natffn  14855  coafval  14928  ismhm  15462  issubm  15470  gsumvalx  15497  issubg  15674  isnsg  15703  gimfn  15782  isgim  15783  isga  15802  cntzval  15832  pmtrfval  15949  psgnfval  15999  odval  16030  odngen  16069  gexval  16070  sylow1lem2  16091  isslw  16100  sylow3lem6  16124  dmdprd  16470  dprdval  16475  dprdvalOLD  16477  ablfac1a  16560  ablfac1b  16561  ablfac1c  16562  ablfac1eu  16564  ablfaclem1  16576  ablfaclem2  16577  ablfaclem3  16578  isirred  16781  issubrg  16845  abvfval  16883  lssset  16993  lmimfn  17085  islmhm  17086  islmim  17121  islbs  17135  rrgval  17336  psrval  17407  gsumbagdiag  17424  psrass1lem  17425  psrbas  17426  psrbasOLD  17427  psrelbas  17428  psraddcl  17432  psrmulfval  17434  psrmulcllem  17436  psrvscaval  17441  psrvscacl  17442  psr0cl  17443  psr0lid  17444  psrnegcl  17445  psrlinv  17446  psrgrp  17447  psrlmod  17450  psr1cl  17451  psrlidmOLD  17453  psrridmOLD  17455  psrdi  17457  psrdir  17458  psrcom  17459  subrgpsr  17469  mvrval  17472  mvrf  17475  mplsubglemOLD  17490  mplsubrg  17497  mplvscaval  17505  mplmonmul  17521  mplbas2  17527  mplbas2OLD  17528  ltbval  17529  opsrval  17532  opsrtoslem2  17542  mplmon2  17551  psrplusgpropd  17665  psropprmul  17668  ocvval  18051  elocv  18052  isobs  18104  islinds  18197  fncld  18585  cnfval  18796  cnpval  18799  iscnp2  18802  1stcfb  19008  kgenf  19073  xkoopn  19121  dfac14  19150  hmeofn  19289  hmeofval  19290  filunirn  19414  alexsubALTlem2  19579  ucnval  19811  iscfilu  19822  ispsmet  19839  ismet  19857  isxmet  19858  xmetunirn  19871  cncfval  20423  ishtpy  20503  isphtpy  20512  om1bas  20562  cfilfval  20734  caufval  20745  iscmet  20754  rrxmet  20866  dyadmax  21037  vitalilem2  21048  vitalilem3  21049  vitalilem4  21050  itg2monolem1  21187  fncpn  21366  elcpn  21367  mdegleb  21494  mdegldg  21496  mdeg0  21500  mdegaddle  21504  mdegvsca  21506  mdegmullem  21508  uc1pval  21570  mon1pval  21572  aannenlem1  21753  aannenlem2  21754  aannenlem3  21755  vmaval  22410  sqff1o  22479  musum  22490  0sgmppw  22496  dchrval  22532  dchrbas  22533  tglnfn  22940  tglnunirn  22941  tglngval  22943  israg  23040  ttgitvval  23063  ebtwntg  23163  lnoval  24087  bloval  24116  hmoval  24145  ubthlem1  24206  ubthlem2  24207  ocval  24618  eigvecval  25235  specval  25237  ordtconlem1  26290  sigaex  26488  isrnsigaOLD  26491  ddemeas  26588  ismbfm  26603  elunirnmbfm  26604  sitgval  26648  eulerpartlemt  26684  eulerpartgbij  26685  eulerpart  26695  ballotlem8  26849  lgamgulmlem5  26949  lgamgulmlem6  26950  lgamgulm2  26952  lgamcvglem  26956  fncvm  27076  iscvm  27078  snmlval  27150  elgiso  27244  fvray  28101  fin2solem  28340  fin2so  28341  cnambfre  28365  istotbnd  28593  isbnd  28604  rngohomval  28695  rngoisoval  28708  idlval  28738  pridlval  28758  maxidlval  28764  isnacs  28965  mzpclval  28986  pell1qrval  29112  pell14qrval  29114  pell1234qrval  29116  mapfien2OLD  29374  pwfi2en  29377  elmnc  29418  itgoval  29443  issdrg  29479  idomodle  29486  idomsubgmo  29488  hashgcdeq  29491  stoweidlem34  29754  wlknwwlknbij2  30271  wlkiswwlkbij2  30278  wlknwwlknvbij  30297  clwwlkbij  30386  clwwlkvbij  30388  clwlksizeeq  30450  rusgranumwlklem1  30492  rusgranumwlklem3  30494  rusgranumwlklem4  30495  rusgranumwwlkg  30502  numclwwlkovg  30605  numclwwlkovq  30617  numclwwlkqhash  30618  numclwwlkovh  30619  bnj110  31685  lshpset  32345  lflset  32426  pats  32652  llnset  32871  lplnset  32895  lvolset  32938  isline  33105  pmapval  33123  paddval  33164  lhpset  33361  ldilset  33475  ltrnset  33484  dilsetN  33519  trnsetN  33522  diafval  34398  diaval  34399  diafn  34401  dicfval  34542  lpolsetN  34849  lcdvadd  34964  lcdsca  34966  lcdvs  34970  mapdval  34995  mapd1o  35015  mapdunirnN  35017
  Copyright terms: Public domain W3C validator