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

Theorem rabex 4598
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 4597 . 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 1767   {crab 2818   _Vcvv 3113
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-in 3483  df-ss 3490
This theorem is referenced by:  rab2ex  4601  frminex  4859  ssimaex  5930  mptrabex  6130  fnpm  7425  mapfien2  7864  inf3lema  8037  cantnffval  8076  dfac2a  8506  kmlem1  8526  axcc4  8815  axdc3lem2  8827  axdc3lem4  8829  pwfseqlem1  9032  nqex  9297  dfuzi  10947  uzval  11080  ixxval  11533  fzval  11670  bitsfval  13925  sadfval  13954  smufval  13979  phicl2  14150  odzval  14170  prmreclem4  14289  prmreclem5  14290  ismre  14838  fnmre  14839  mrisval  14878  isacs  14899  ismon  14982  isnat  15167  natffn  15169  coafval  15242  ismhm  15776  issubm  15785  gsumvalx  15812  issubg  15993  isnsg  16022  gimfn  16101  isgim  16102  isga  16121  cntzval  16151  pmtrfval  16268  psgnfval  16318  odval  16351  odngen  16390  gexval  16391  sylow1lem2  16412  isslw  16421  sylow3lem6  16445  dmdprd  16817  dprdval  16822  dprdvalOLD  16824  ablfac1a  16907  ablfac1b  16908  ablfac1c  16909  ablfac1eu  16911  ablfaclem1  16923  ablfaclem2  16924  ablfaclem3  16925  isirred  17129  isrim0  17153  issubrg  17209  abvfval  17247  lssset  17360  lmimfn  17452  islmhm  17453  islmim  17488  islbs  17502  rrgval  17703  psrval  17779  gsumbagdiag  17796  psrass1lem  17797  psrbas  17798  psrbasOLD  17799  psrelbas  17800  psraddcl  17804  psrmulfval  17806  psrmulcllem  17808  psrvscaval  17813  psrvscacl  17814  psr0cl  17815  psr0lid  17816  psrnegcl  17817  psrlinv  17818  psrgrp  17819  psrlmod  17822  psr1cl  17823  psrlidmOLD  17825  psrridmOLD  17827  psrdi  17829  psrdir  17830  psrcom  17832  subrgpsr  17842  mvrval  17845  mvrf  17848  mplsubglemOLD  17863  mplsubrg  17870  mplvscaval  17878  mplmonmul  17894  mplbas2  17902  mplbas2OLD  17903  ltbval  17904  opsrval  17907  opsrtoslem2  17917  mplmon2  17926  psrplusgpropd  18045  psropprmul  18047  ocvval  18462  elocv  18463  isobs  18515  islinds  18608  scmatval  18770  fncld  19286  cnfval  19497  cnpval  19500  iscnp2  19503  1stcfb  19709  kgenf  19774  xkoopn  19822  dfac14  19851  hmeofn  19990  hmeofval  19991  filunirn  20115  alexsubALTlem2  20280  ucnval  20512  iscfilu  20523  ispsmet  20540  ismet  20558  isxmet  20559  xmetunirn  20572  cncfval  21124  ishtpy  21204  isphtpy  21213  om1bas  21263  cfilfval  21435  caufval  21446  iscmet  21455  rrxmet  21567  dyadmax  21739  vitalilem2  21750  vitalilem3  21751  vitalilem4  21752  itg2monolem1  21889  fncpn  22068  elcpn  22069  mdegleb  22196  mdegldg  22198  mdeg0  22202  mdegaddle  22206  mdegvsca  22208  mdegmullem  22210  uc1pval  22272  mon1pval  22274  aannenlem1  22455  aannenlem2  22456  aannenlem3  22457  vmaval  23112  sqff1o  23181  musum  23192  0sgmppw  23198  dchrval  23234  dchrbas  23235  tglnfn  23659  tglnunirn  23660  tglngval  23663  israg  23779  ttgitvval  23858  ebtwntg  23958  wlknwwlknbij2  24387  wlkiswwlkbij2  24394  wlknwwlknvbij  24413  clwwlkbij  24472  clwwlkvbij  24474  clwlksizeeq  24525  rusgranumwlklem1  24622  rusgranumwlklem3  24624  rusgranumwlklem4  24625  rusgranumwwlkg  24632  numclwwlkovg  24761  numclwwlkovq  24773  numclwwlkqhash  24774  numclwwlkovh  24775  lnoval  25340  bloval  25369  hmoval  25398  ubthlem1  25459  ubthlem2  25460  ocval  25871  eigvecval  26488  specval  26490  ordtconlem1  27539  sigaex  27746  isrnsigaOLD  27749  ddemeas  27845  ismbfm  27860  elunirnmbfm  27861  sitgval  27911  eulerpartlemt  27947  eulerpartgbij  27948  eulerpart  27958  ballotlem8  28112  lgamgulmlem5  28212  lgamgulmlem6  28213  lgamgulm2  28215  lgamcvglem  28219  fncvm  28339  iscvm  28341  snmlval  28413  elgiso  28508  fvray  29365  fin2solem  29613  fin2so  29614  cnambfre  29638  istotbnd  29866  isbnd  29877  rngohomval  29968  rngoisoval  29981  idlval  30011  pridlval  30031  maxidlval  30037  isnacs  30238  mzpclval  30259  pell1qrval  30384  pell14qrval  30386  pell1234qrval  30388  mapfien2OLD  30646  pwfi2en  30649  elmnc  30690  itgoval  30715  issdrg  30751  idomodle  30758  idomsubgmo  30760  hashgcdeq  30763  stoweidlem34  31334  fourierdlem2  31409  fourierdlem3  31410  usgsizedg  31864  usgsizedgALT  31865  usgsizedgALT2  31866  fiusgedgfi  31901  fiusgedgfiALT  31902  assintopval  31953  bnj110  32995  lshpset  33775  lflset  33856  pats  34082  llnset  34301  lplnset  34325  lvolset  34368  isline  34535  pmapval  34553  paddval  34594  lhpset  34791  ldilset  34905  ltrnset  34914  dilsetN  34949  trnsetN  34952  diafval  35828  diaval  35829  diafn  35831  dicfval  35972  lpolsetN  36279  lcdvadd  36394  lcdsca  36396  lcdvs  36400  mapdval  36425  mapd1o  36445  mapdunirnN  36447
  Copyright terms: Public domain W3C validator