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

Theorem rabex 5290
Description: Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 19-Jul-1996.)
Hypothesis
Ref Expression
rabex.1 𝐴 ∈ V
Assertion
Ref Expression
rabex {𝑥𝐴𝜑} ∈ V
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rabex
StepHypRef Expression
1 rabex.1 . 2 𝐴 ∈ V
2 rabexg 5289 . 2 (𝐴 ∈ V → {𝑥𝐴𝜑} ∈ V)
31, 2ax-mp 5 1 {𝑥𝐴𝜑} ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  {crab 3408  Vcvv 3446
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-sep 5257
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3409  df-v 3448  df-in 3918  df-ss 3928
This theorem is referenced by:  rab2ex  5293  frminex  5614  ssimaex  6927  fvmptrabfv  6980  mptrabex  7176  fnpm  8774  inf3lema  9561  dfac2a  10066  kmlem1  10087  axcc4  10376  axdc3lem2  10388  axdc3lem4  10390  pwfseqlem1  10595  dfuzi  12595  uzval  12766  ixxval  13273  fzval  13427  bitsfval  16304  sadfval  16333  smufval  16358  phicl2  16641  hashgcdeq  16662  prmreclem4  16792  prmreclem5  16793  ismre  17471  fnmre  17472  mrisval  17511  isacs  17532  ismon  17617  isnat  17835  natffn  17837  initofn  17874  termofn  17875  initoval  17880  termoval  17881  coafval  17951  ismhm  18604  issubm  18615  issubg  18929  isnsg  18958  gimfn  19052  isgim  19053  isga  19072  cntzval  19102  odfval  19315  odngen  19360  gexval  19361  isslw  19391  ablfac1a  19849  ablfac1b  19850  ablfac1c  19851  ablfac1eu  19853  ablfaclem1  19865  ablfaclem2  19866  ablfaclem3  19867  isirred  20129  isrim0OLD  20155  isrim0  20157  issubrg  20225  issdrg  20264  abvfval  20280  lssset  20397  lmimfn  20490  islmhm  20491  islmim  20526  islbs  20540  rrgval  20760  ocvval  21074  elocv  21075  isobs  21129  islinds  21218  psrval  21320  psraddcl  21354  psrvscacl  21364  psrgrp  21369  psrgrpOLD  21370  psrlmod  21373  subrgpsr  21391  mvrf  21396  mplsubrg  21414  mplmonmul  21440  mplbas2  21446  opsrval  21450  mhpval  21533  mhpmulcl  21542  mhpinvcl  21545  psrplusgpropd  21610  psropprmul  21612  scmatval  21856  fncld  22376  cnfval  22587  cnpval  22590  iscnp2  22593  1stcfb  22799  kgenf  22895  xkoopn  22943  dfac14  22972  hmeofn  23111  hmeofval  23112  filunirn  23236  alexsubALTlem2  23402  ucnval  23632  iscfilu  23643  ispsmet  23660  ismet  23679  isxmet  23680  xmetunirn  23693  cncfval  24254  ishtpy  24338  isphtpy  24347  om1bas  24397  cfilfval  24631  caufval  24642  iscmet  24651  dyadmax  24965  vitalilem2  24976  vitalilem3  24977  vitalilem4  24978  itg2monolem1  25118  fncpn  25300  elcpn  25301  mdeg0  25438  mdegaddle  25442  mdegvsca  25444  uc1pval  25507  mon1pval  25509  aannenlem1  25691  aannenlem2  25692  aannenlem3  25693  vmaval  26465  sqff1o  26534  musum  26543  dchrval  26585  dchrbas  26586  leftval  27196  rightval  27197  leftf  27198  rightf  27199  tglnfn  27492  tglnunirn  27493  tglngval  27496  israg  27642  iseqlg  27812  ttgitvval  27833  ebtwntg  27934  incistruhgr  28033  usgredgleordALT  28185  vtxdun  28432  vtxdlfgrval  28436  vtxd0nedgb  28439  vtxdushgrfvedglem  28440  vtxdushgrfvedg  28441  vtxdusgr0edgnelALT  28447  1loopgrvd2  28454  usgrvd0nedg  28484  rusgrnumwrdl2  28537  ewlksfval  28552  wwlksn  28785  wspthsn  28796  iswwlksnon  28801  iswspthsnon  28804  wlknwwlksnen  28837  wwlksnexthasheq  28851  rusgrnumwlkg  28925  clwlkclwwlken  28959  clwwlkn  28973  clwwlken  28999  clwlkssizeeq  29032  clwwlknon  29037  clwwlk0on0  29039  konigsberglem5  29203  fusgreg2wsplem  29280  fusgreghash2wsp  29285  2clwwlk  29294  clwwlknonclwlknonen  29310  numclwlk1lem2  29317  numclwwlkovh0  29319  numclwwlkovq  29321  numclwwlkqhash  29322  lnoval  29697  bloval  29726  hmoval  29755  ubthlem1  29815  ubthlem2  29816  ocval  30225  eigvecval  30841  specval  30843  rabfodom  31435  fpwrelmap  31653  nsgmgc  32193  mxidlval  32233  ssmxidl  32242  rprmval  32264  locfinreflem  32424  rspectopn  32451  zarcls1  32453  zarclsun  32454  zarclsiin  32455  zarclsint  32456  zarclssn  32457  zarcls  32458  zartopn  32459  zar0ring  32462  zart0  32463  zarmxt1  32464  zarcmplem  32465  rhmpreimacnlem  32468  rhmpreimacn  32469  ordtconnlem1  32508  sigaex  32712  ddemeas  32838  ismbfm  32853  elunirnmbfm  32854  eulerpart  32985  ballotlem8  33139  reprval  33226  bnj110  33473  fncvm  33854  iscvm  33856  snmlval  33928  satfv1  33960  satfdm  33966  satffunlem1lem2  34000  satfv0fvfmla0  34010  satfv1fvfmla1  34020  mpstval  34132  fvray  34729  icoreval  35827  fin2solem  36067  fin2so  36068  poimirlem4  36085  cnambfre  36129  istotbnd  36231  isbnd  36242  rngohomval  36426  rngoisoval  36439  idlval  36475  pridlval  36495  maxidlval  36501  lshpset  37443  lflset  37524  pats  37750  llnset  37971  lplnset  37995  lvolset  38038  isline  38205  pmapval  38223  paddval  38264  lhpset  38461  ldilset  38575  ltrnset  38584  dilsetN  38619  trnsetN  38622  diaval  39498  diafn  39500  lpolsetN  39948  lcdvadd  40063  lcdsca  40065  lcdvs  40069  mapdval  40094  mapd1o  40114  mhmcompl  40739  mhmcoaddmpl  40742  rhmcomulmpl  40743  mhphf  40774  prjcrvval  40973  isnacs  41030  mzpclval  41051  pell1qrval  41172  pell14qrval  41174  pell1234qrval  41176  elmnc  41466  itgoval  41491  idomodle  41526  idomsubgmo  41528  k0004val  42429  icof  43447  elicores  43778  dvnprodlem1  44194  dvnprodlem2  44195  dvnprodlem3  44196  stoweidlem34  44282  fourierdlem2  44357  fourierdlem3  44358  etransclem12  44494  etransclem33  44515  ovnval2b  44800  volicorescl  44801  ovncvrrp  44812  ovnsubaddlem1  44818  ovncvr2  44859  issmflem  44975  smfaddlem1  45011  smfaddlem2  45012  smflimlem1  45019  fvmptrabdm  45532  iccpval  45614  fppr  45925  ismgmhm  46084  issubmgm  46090  assintopval  46146  rnghmfn  46195  rnghmval  46196  isrngisom  46201  rngchomrnghmresALTV  46301  bigoval  46642  elbigofrcl  46643  line  46825  rrxline  46827  sphere  46840  rrxsphere  46841
  Copyright terms: Public domain W3C validator