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

Theorem rabex 5007
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 5006 . 2 (𝐴 ∈ V → {𝑥𝐴𝜑} ∈ V)
31, 2ax-mp 5 1 {𝑥𝐴𝜑} ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2156  {crab 3100  Vcvv 3391
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-rab 3105  df-v 3393  df-in 3776  df-ss 3783
This theorem is referenced by:  rab2ex  5010  frminex  5291  ssimaex  6484  fvmptrabfv  6530  mptrabex  6713  fnpm  8100  inf3lema  8768  dfac2a  9235  kmlem1  9257  axcc4  9546  axdc3lem2  9558  axdc3lem4  9560  pwfseqlem1  9765  dfuzi  11734  uzval  11906  ixxval  12401  fzval  12551  bitsfval  15364  sadfval  15393  smufval  15418  phicl2  15690  hashgcdeq  15711  prmreclem4  15840  prmreclem5  15841  ismre  16455  fnmre  16456  mrisval  16495  isacs  16516  ismon  16597  isnat  16811  natffn  16813  initoval  16851  termoval  16852  coafval  16918  ismhm  17542  issubm  17552  issubg  17796  isnsg  17825  gimfn  17905  isgim  17906  isga  17925  cntzval  17955  odngen  18193  gexval  18194  isslw  18224  ablfac1a  18670  ablfac1b  18671  ablfac1c  18672  ablfac1eu  18674  ablfaclem1  18686  ablfaclem2  18687  ablfaclem3  18688  isirred  18901  isrim0  18927  issubrg  18984  abvfval  19022  lssset  19138  lmimfn  19233  islmhm  19234  islmim  19269  islbs  19283  rrgval  19496  psrval  19571  psraddcl  19592  psrvscacl  19602  psrgrp  19607  psrlmod  19610  subrgpsr  19628  mvrf  19633  mplsubrg  19649  mplmonmul  19673  mplbas2  19679  opsrval  19683  psrplusgpropd  19814  psropprmul  19816  ocvval  20221  elocv  20222  isobs  20274  islinds  20358  scmatval  20521  fncld  21040  cnfval  21251  cnpval  21254  iscnp2  21257  1stcfb  21462  kgenf  21558  xkoopn  21606  dfac14  21635  hmeofn  21774  hmeofval  21775  filunirn  21899  alexsubALTlem2  22065  ucnval  22294  iscfilu  22305  ispsmet  22322  ismet  22341  isxmet  22342  xmetunirn  22355  cncfval  22904  ishtpy  22984  isphtpy  22993  om1bas  23043  cfilfval  23274  caufval  23285  iscmet  23294  dyadmax  23579  vitalilem2  23590  vitalilem3  23591  vitalilem4  23592  itg2monolem1  23731  fncpn  23910  elcpn  23911  mdegleb  24038  mdeg0  24044  mdegaddle  24048  mdegvsca  24050  uc1pval  24113  mon1pval  24115  aannenlem1  24297  aannenlem2  24298  aannenlem3  24299  vmaval  25053  sqff1o  25122  musum  25131  0sgmppw  25137  dchrval  25173  dchrbas  25174  tglnfn  25656  tglnunirn  25657  tglngval  25660  israg  25806  iseqlg  25961  ttgitvval  25976  ebtwntg  26076  incistruhgr  26188  usgredgleordALT  26342  uvtxavalOLD  26506  vtxdun  26605  vtxdlfgrval  26609  vtxd0nedgb  26612  vtxdushgrfvedglem  26613  vtxdushgrfvedg  26614  vtxdusgr0edgnelALT  26620  1loopgrvd2  26627  usgrvd0nedg  26657  vtxdginducedm1lem4  26666  rusgrnumwrdl2  26710  ewlksfval  26725  wwlksn  26958  wspthsn  26970  iswwlksnon  26975  iswwlksnonOLD  26976  iswspthsnon  26979  iswspthsnonOLD  26980  wlknwwlksnen  27021  wwlksnexthasheq  27040  rusgrnumwlkg  27119  clwlkclwwlken  27155  clwwlkn  27171  clwwlknOLD  27172  clwwlken  27201  clwlkssizeeq  27249  clwlkssizeeqOLD  27250  clwwlknon  27255  clwwlknonOLD  27256  clwwlk0on0  27259  konigsberglem5  27429  fusgreg2wsplem  27508  fusgreghash2wsp  27513  2clwwlk  27524  numclwwlkovgOLD  27528  clwwlknonclwlknonen  27543  numclwlk1lem2  27550  numclwwlkovh0  27552  numclwwlkovq  27554  numclwwlkqhash  27555  numclwwlkovhOLD  27562  lnoval  27935  bloval  27964  hmoval  27993  ubthlem1  28054  ubthlem2  28055  ocval  28467  eigvecval  29083  specval  29085  rabfodom  29669  fpwrelmap  29835  locfinreflem  30232  ordtconnlem1  30295  sigaex  30497  isrnsigaOLD  30500  ddemeas  30624  ismbfm  30639  elunirnmbfm  30640  eulerpart  30769  ballotlem8  30923  reprval  31013  bnj110  31251  fncvm  31562  iscvm  31564  snmlval  31636  mpstval  31755  fvray  32569  icoreval  33517  fin2solem  33708  fin2so  33709  poimirlem4  33726  cnambfre  33770  istotbnd  33879  isbnd  33890  rngohomval  34074  rngoisoval  34087  idlval  34123  pridlval  34143  maxidlval  34149  lshpset  34758  lflset  34839  pats  35065  llnset  35285  lplnset  35309  lvolset  35352  isline  35519  pmapval  35537  paddval  35578  lhpset  35775  ldilset  35889  ltrnset  35898  dilsetN  35934  trnsetN  35937  diaval  36813  diafn  36815  lpolsetN  37263  lcdvadd  37378  lcdsca  37380  lcdvs  37384  mapdval  37409  mapd1o  37429  isnacs  37769  mzpclval  37790  pell1qrval  37912  pell14qrval  37914  pell1234qrval  37916  elmnc  38207  itgoval  38232  issdrg  38268  idomodle  38275  idomsubgmo  38277  k0004val  38948  icof  39898  elicores  40240  dvnprodlem1  40641  dvnprodlem2  40642  dvnprodlem3  40643  stoweidlem34  40730  fourierdlem2  40805  fourierdlem3  40806  etransclem12  40942  etransclem33  40963  ovnval2b  41248  volicorescl  41249  ovncvrrp  41260  ovnsubaddlem1  41266  ovncvr2  41307  issmflem  41418  smfaddlem1  41453  smfaddlem2  41454  smflimlem1  41461  fvmptrabdm  41883  iccpval  41926  ismgmhm  42351  issubmgm  42357  assintopval  42409  rnghmfn  42458  rnghmval  42459  isrngisom  42464  rngchomrnghmresALTV  42564  bigoval  42911  elbigofrcl  42912
  Copyright terms: Public domain W3C validator