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

Theorem rabex 4557
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 4556 . 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 1889   {crab 2743   _Vcvv 3047
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-rab 2748  df-v 3049  df-in 3413  df-ss 3420
This theorem is referenced by:  rab2ex  4560  frminex  4817  ssimaex  5935  mptrabex  6142  fnpm  7485  inf3lema  8134  dfac2a  8565  kmlem1  8585  axcc4  8874  axdc3lem2  8886  axdc3lem4  8888  pwfseqlem1  9088  dfuzi  11033  uzval  11168  ixxval  11650  fzval  11793  bitsfval  14408  sadfval  14438  smufval  14463  phicl2  14728  prmreclem4  14875  prmreclem5  14876  ismre  15508  fnmre  15509  mrisval  15548  isacs  15569  ismon  15650  isnat  15864  natffn  15866  initoval  15904  termoval  15905  coafval  15971  ismhm  16596  issubm  16606  issubg  16829  isnsg  16858  gimfn  16937  isgim  16938  isga  16957  cntzval  16987  odngen  17238  gexval  17239  gexvalOLD  17241  isslw  17272  ablfac1a  17714  ablfac1b  17715  ablfac1c  17716  ablfac1eu  17718  ablfaclem1  17730  ablfaclem2  17731  ablfaclem3  17732  isirred  17939  isrim0  17963  issubrg  18020  abvfval  18058  lssset  18169  lmimfn  18261  islmhm  18262  islmim  18297  islbs  18311  rrgval  18523  psrval  18598  psraddcl  18619  psrvscacl  18629  psrgrp  18634  psrlmod  18637  subrgpsr  18655  mvrf  18660  mplsubrg  18676  mplmonmul  18700  mplbas2  18706  opsrval  18710  psrplusgpropd  18841  psropprmul  18843  ocvval  19242  elocv  19243  isobs  19295  islinds  19379  scmatval  19541  fncld  20049  cnfval  20261  cnpval  20264  iscnp2  20267  1stcfb  20472  kgenf  20568  xkoopn  20616  dfac14  20645  hmeofn  20784  hmeofval  20785  filunirn  20909  alexsubALTlem2  21075  ucnval  21304  iscfilu  21315  ispsmet  21332  ismet  21350  isxmet  21351  xmetunirn  21364  cncfval  21932  ishtpy  22015  isphtpy  22024  om1bas  22074  cfilfval  22246  caufval  22257  iscmet  22266  dyadmax  22568  vitalilem2  22579  vitalilem3  22580  vitalilem4  22581  itg2monolem1  22720  fncpn  22899  elcpn  22900  mdegleb  23025  mdeg0  23031  mdegaddle  23035  mdegvsca  23037  uc1pval  23102  mon1pval  23104  aannenlem1  23296  aannenlem2  23297  aannenlem3  23298  vmaval  24052  sqff1o  24121  musum  24132  0sgmppw  24138  dchrval  24174  dchrbas  24175  tglnfn  24604  tglnunirn  24605  tglngval  24608  israg  24754  iseqlg  24909  ttgitvval  24924  ebtwntg  25024  clwlksizeeq  25592  rusgranumwlklem1  25689  rusgranumwlklem3  25691  rusgranumwlklem4  25692  rusgranumwwlkg  25699  numclwwlkovf  25821  numclwwlkovg  25827  numclwwlkovq  25839  numclwwlkqhash  25840  numclwwlkovh  25841  lnoval  26405  bloval  26434  hmoval  26463  ubthlem1  26524  ubthlem2  26525  ocval  26945  eigvecval  27561  specval  27563  rabfodom  28152  fpwrelmap  28330  locfinreflem  28679  ordtconlem1  28742  sigaex  28943  isrnsigaOLD  28946  ddemeas  29071  ismbfm  29086  elunirnmbfm  29087  eulerpart  29227  ballotlem8  29381  ballotlem8OLD  29419  bnj110  29681  fncvm  29992  iscvm  29994  snmlval  30066  mpstval  30185  elgiso  30326  fvray  30920  icoreval  31768  fin2solem  31943  fin2so  31944  poimirlem4  31956  cnambfre  32001  istotbnd  32113  isbnd  32124  rngohomval  32215  rngoisoval  32228  idlval  32258  pridlval  32278  maxidlval  32284  lshpset  32556  lflset  32637  pats  32863  llnset  33082  lplnset  33106  lvolset  33149  isline  33316  pmapval  33334  paddval  33375  lhpset  33572  ldilset  33686  ltrnset  33695  dilsetN  33731  trnsetN  33734  diaval  34612  diafn  34614  lpolsetN  35062  lcdvadd  35177  lcdsca  35179  lcdvs  35183  mapdval  35208  mapd1o  35228  isnacs  35558  mzpclval  35579  pell1qrval  35704  pell14qrval  35706  pell1234qrval  35708  elmnc  36007  itgoval  36039  issdrg  36075  idomodle  36082  idomsubgmo  36084  hashgcdeq  36087  elicores  37645  dvnprodlem1  37831  dvnprodlem2  37832  dvnprodlem3  37833  stoweidlem34  37905  fourierdlem2  37981  fourierdlem3  37982  etransclem12  38121  etransclem33  38142  ovnval2b  38384  volicorescl  38385  ovncvrrp  38396  ovnsubaddlem1  38402  ovncvr2  38443  iccpval  38739  incistruhgr  39181  usgredgaleordALT  39321  nbedgusgr  39456  uvtxaval  39469  vtxduhgrun  39548  vtxdumgrval  39550  vtxdushgrfvedglem  39552  vtxdushgrfvedg  39553  uhgrvd0nedgb  39555  vtxdusgr0edgnelALT  39560  uspgrloopvd2  39567  hashnbusgrvd  39575  usgrvd0nedg  39580  ewlksfval  39628  usgsizedg  39811  usgsizedgALT  39812  usgsizedgALT2  39813  fiusgedgfi  39848  fiusgedgfiALT  39849  ismgmhm  39887  issubmgm  39893  assintopval  39945  rnghmfn  39994  rnghmval  39995  isrngisom  40000  rngchomrnghmresALTV  40102  bigoval  40464  elbigofrcl  40465
  Copyright terms: Public domain W3C validator