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

Theorem rabex 4588
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 4587 . 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 1804   {crab 2797   _Vcvv 3095
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-v 3097  df-in 3468  df-ss 3475
This theorem is referenced by:  rab2ex  4591  frminex  4849  ssimaex  5923  mptrabex  6129  fnpm  7430  inf3lema  8044  dfac2a  8513  kmlem1  8533  axcc4  8822  axdc3lem2  8834  axdc3lem4  8836  pwfseqlem1  9039  dfuzi  10960  uzval  11094  ixxval  11548  fzval  11685  bitsfval  14055  sadfval  14084  smufval  14109  phicl2  14280  prmreclem4  14419  prmreclem5  14420  ismre  14969  fnmre  14970  mrisval  15009  isacs  15030  ismon  15110  isnat  15295  natffn  15297  coafval  15370  ismhm  15947  issubm  15957  issubg  16180  isnsg  16209  gimfn  16288  isgim  16289  isga  16308  cntzval  16338  odngen  16576  gexval  16577  isslw  16607  dprdvalOLD  17015  ablfac1a  17099  ablfac1b  17100  ablfac1c  17101  ablfac1eu  17103  ablfaclem1  17115  ablfaclem2  17116  ablfaclem3  17117  isirred  17327  isrim0  17351  issubrg  17408  abvfval  17446  lssset  17559  lmimfn  17651  islmhm  17652  islmim  17687  islbs  17701  rrgval  17914  psrval  17990  psrbasOLD  18010  psraddcl  18015  psrvscacl  18025  psrgrp  18030  psrlmod  18033  psrlidmOLD  18036  psrridmOLD  18038  subrgpsr  18053  mvrf  18059  mplsubglemOLD  18074  mplsubrg  18081  mplmonmul  18105  mplbas2  18113  mplbas2OLD  18114  opsrval  18118  psrplusgpropd  18256  psropprmul  18258  ocvval  18676  elocv  18677  isobs  18729  islinds  18822  scmatval  18984  fncld  19501  cnfval  19712  cnpval  19715  iscnp2  19718  1stcfb  19924  kgenf  20020  xkoopn  20068  dfac14  20097  hmeofn  20236  hmeofval  20237  filunirn  20361  alexsubALTlem2  20526  ucnval  20758  iscfilu  20769  ispsmet  20786  ismet  20804  isxmet  20805  xmetunirn  20818  cncfval  21370  ishtpy  21450  isphtpy  21459  om1bas  21509  cfilfval  21681  caufval  21692  iscmet  21701  dyadmax  21985  vitalilem2  21996  vitalilem3  21997  vitalilem4  21998  itg2monolem1  22135  fncpn  22314  elcpn  22315  mdegleb  22442  mdeg0  22448  mdegaddle  22452  mdegvsca  22454  uc1pval  22518  mon1pval  22520  aannenlem1  22702  aannenlem2  22703  aannenlem3  22704  vmaval  23365  sqff1o  23434  musum  23445  0sgmppw  23451  dchrval  23487  dchrbas  23488  tglnfn  23912  tglnunirn  23913  tglngval  23916  israg  24052  ttgitvval  24163  ebtwntg  24263  clwlksizeeq  24830  rusgranumwlklem1  24927  rusgranumwlklem3  24929  rusgranumwlklem4  24930  rusgranumwwlkg  24937  numclwwlkovf  25059  numclwwlkovg  25065  numclwwlkovq  25077  numclwwlkqhash  25078  numclwwlkovh  25079  lnoval  25645  bloval  25674  hmoval  25703  ubthlem1  25764  ubthlem2  25765  ocval  26176  eigvecval  26793  specval  26795  rabfodom  27382  fpwrelmap  27534  locfinreflem  27821  ordtconlem1  27884  sigaex  28087  isrnsigaOLD  28090  ddemeas  28186  ismbfm  28201  elunirnmbfm  28202  eulerpart  28299  ballotlem8  28453  fncvm  28680  iscvm  28682  snmlval  28754  mpstval  28873  elgiso  29014  fvray  29767  fin2solem  30015  fin2so  30016  cnambfre  30039  istotbnd  30241  isbnd  30252  rngohomval  30343  rngoisoval  30356  idlval  30386  pridlval  30406  maxidlval  30412  isnacs  30612  mzpclval  30633  pell1qrval  30758  pell14qrval  30760  pell1234qrval  30762  mapfien2OLD  31018  elmnc  31061  itgoval  31086  issdrg  31122  idomodle  31129  idomsubgmo  31131  hashgcdeq  31134  dvnprodlem1  31697  dvnprodlem2  31698  dvnprodlem3  31699  stoweidlem34  31770  fourierdlem2  31845  fourierdlem3  31846  etransclem12  31983  etransclem31  32002  etransclem33  32004  usgsizedg  32349  usgsizedgALT  32350  usgsizedgALT2  32351  fiusgedgfi  32386  fiusgedgfiALT  32387  ismgmhm  32425  issubmgm  32431  assintopval  32482  rnghmfn  32531  rnghmval  32532  isrngisom  32537  rngchomrnghmresOLD  32679  bnj110  33784  lshpset  34578  lflset  34659  pats  34885  llnset  35104  lplnset  35128  lvolset  35171  isline  35338  pmapval  35356  paddval  35397  lhpset  35594  ldilset  35708  ltrnset  35717  dilsetN  35753  trnsetN  35756  diaval  36634  diafn  36636  lpolsetN  37084  lcdvadd  37199  lcdsca  37201  lcdvs  37205  mapdval  37230  mapd1o  37250
  Copyright terms: Public domain W3C validator