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

Theorem rabex 4529
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 4528 . 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 1836   {crab 2746   _Vcvv 3047
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-sep 4501
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-rab 2751  df-v 3049  df-in 3409  df-ss 3416
This theorem is referenced by:  rab2ex  4532  frminex  4786  ssimaex  5852  mptrabex  6061  fnpm  7364  inf3lema  7973  dfac2a  8441  kmlem1  8461  axcc4  8750  axdc3lem2  8762  axdc3lem4  8764  pwfseqlem1  8965  dfuzi  10888  uzval  11021  ixxval  11476  fzval  11613  bitsfval  14094  sadfval  14123  smufval  14148  phicl2  14319  prmreclem4  14458  prmreclem5  14459  ismre  15016  fnmre  15017  mrisval  15056  isacs  15077  ismon  15158  isnat  15372  natffn  15374  initoval  15412  termoval  15413  coafval  15479  ismhm  16104  issubm  16114  issubg  16337  isnsg  16366  gimfn  16445  isgim  16446  isga  16465  cntzval  16495  odngen  16733  gexval  16734  isslw  16764  dprdvalOLD  17168  ablfac1a  17252  ablfac1b  17253  ablfac1c  17254  ablfac1eu  17256  ablfaclem1  17268  ablfaclem2  17269  ablfaclem3  17270  isirred  17480  isrim0  17504  issubrg  17561  abvfval  17599  lssset  17712  lmimfn  17804  islmhm  17805  islmim  17840  islbs  17854  rrgval  18067  psrval  18143  psrbasOLD  18163  psraddcl  18168  psrvscacl  18178  psrgrp  18183  psrlmod  18186  psrlidmOLD  18189  psrridmOLD  18191  subrgpsr  18206  mvrf  18212  mplsubglemOLD  18227  mplsubrg  18234  mplmonmul  18258  mplbas2  18266  mplbas2OLD  18267  opsrval  18271  psrplusgpropd  18409  psropprmul  18411  ocvval  18808  elocv  18809  isobs  18861  islinds  18948  scmatval  19110  fncld  19627  cnfval  19839  cnpval  19842  iscnp2  19845  1stcfb  20050  kgenf  20146  xkoopn  20194  dfac14  20223  hmeofn  20362  hmeofval  20363  filunirn  20487  alexsubALTlem2  20652  ucnval  20884  iscfilu  20895  ispsmet  20912  ismet  20930  isxmet  20931  xmetunirn  20944  cncfval  21496  ishtpy  21576  isphtpy  21585  om1bas  21635  cfilfval  21807  caufval  21818  iscmet  21827  dyadmax  22111  vitalilem2  22122  vitalilem3  22123  vitalilem4  22124  itg2monolem1  22261  fncpn  22440  elcpn  22441  mdegleb  22568  mdeg0  22574  mdegaddle  22578  mdegvsca  22580  uc1pval  22644  mon1pval  22646  aannenlem1  22828  aannenlem2  22829  aannenlem3  22830  vmaval  23523  sqff1o  23592  musum  23603  0sgmppw  23609  dchrval  23645  dchrbas  23646  tglnfn  24075  tglnunirn  24076  tglngval  24079  israg  24215  ttgitvval  24327  ebtwntg  24427  clwlksizeeq  24994  rusgranumwlklem1  25091  rusgranumwlklem3  25093  rusgranumwlklem4  25094  rusgranumwwlkg  25101  numclwwlkovf  25223  numclwwlkovg  25229  numclwwlkovq  25241  numclwwlkqhash  25242  numclwwlkovh  25243  lnoval  25805  bloval  25834  hmoval  25863  ubthlem1  25924  ubthlem2  25925  ocval  26336  eigvecval  26952  specval  26954  rabfodom  27545  fpwrelmap  27736  locfinreflem  28028  ordtconlem1  28091  sigaex  28289  isrnsigaOLD  28292  ddemeas  28400  ismbfm  28415  elunirnmbfm  28416  eulerpart  28540  ballotlem8  28694  fncvm  28927  iscvm  28929  snmlval  29001  mpstval  29120  elgiso  29261  fvray  29980  fin2solem  30240  fin2so  30241  cnambfre  30264  istotbnd  30467  isbnd  30478  rngohomval  30569  rngoisoval  30582  idlval  30612  pridlval  30632  maxidlval  30638  isnacs  30838  mzpclval  30859  pell1qrval  30983  pell14qrval  30985  pell1234qrval  30987  mapfien2OLD  31244  elmnc  31289  itgoval  31314  issdrg  31350  idomodle  31357  idomsubgmo  31359  hashgcdeq  31362  dvnprodlem1  31944  dvnprodlem2  31945  dvnprodlem3  31946  stoweidlem34  32017  fourierdlem2  32092  fourierdlem3  32093  etransclem12  32230  etransclem33  32251  usgsizedg  32748  usgsizedgALT  32749  usgsizedgALT2  32750  fiusgedgfi  32785  fiusgedgfiALT  32786  ismgmhm  32824  issubmgm  32830  assintopval  32882  rnghmfn  32931  rnghmval  32932  isrngisom  32937  rngchomrnghmresALTV  33039  bigoval  33405  elbigofrcl  33406  bnj110  34298  lshpset  35151  lflset  35232  pats  35458  llnset  35677  lplnset  35701  lvolset  35744  isline  35911  pmapval  35929  paddval  35970  lhpset  36167  ldilset  36281  ltrnset  36290  dilsetN  36326  trnsetN  36329  diaval  37207  diafn  37209  lpolsetN  37657  lcdvadd  37772  lcdsca  37774  lcdvs  37778  mapdval  37803  mapd1o  37823
  Copyright terms: Public domain W3C validator