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

Theorem rabex 4964
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 4963 . 2 (𝐴 ∈ V → {𝑥𝐴𝜑} ∈ V)
31, 2ax-mp 5 1 {𝑥𝐴𝜑} ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2139  {crab 3054  Vcvv 3340
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-in 3722  df-ss 3729
This theorem is referenced by:  rab2ex  4967  frminex  5246  ssimaex  6425  fvmptrabfv  6471  mptrabex  6652  fnpm  8031  inf3lema  8694  dfac2a  9142  kmlem1  9164  axcc4  9453  axdc3lem2  9465  axdc3lem4  9467  pwfseqlem1  9672  dfuzi  11660  uzval  11881  ixxval  12376  fzval  12521  bitsfval  15347  sadfval  15376  smufval  15401  phicl2  15675  hashgcdeq  15696  prmreclem4  15825  prmreclem5  15826  ismre  16452  fnmre  16453  mrisval  16492  isacs  16513  ismon  16594  isnat  16808  natffn  16810  initoval  16848  termoval  16849  coafval  16915  ismhm  17538  issubm  17548  issubg  17795  isnsg  17824  gimfn  17904  isgim  17905  isga  17924  cntzval  17954  odngen  18192  gexval  18193  isslw  18223  ablfac1a  18668  ablfac1b  18669  ablfac1c  18670  ablfac1eu  18672  ablfaclem1  18684  ablfaclem2  18685  ablfaclem3  18686  isirred  18899  isrim0  18925  issubrg  18982  abvfval  19020  lssset  19136  lmimfn  19228  islmhm  19229  islmim  19264  islbs  19278  rrgval  19489  psrval  19564  psraddcl  19585  psrvscacl  19595  psrgrp  19600  psrlmod  19603  subrgpsr  19621  mvrf  19626  mplsubrg  19642  mplmonmul  19666  mplbas2  19672  opsrval  19676  psrplusgpropd  19808  psropprmul  19810  ocvval  20213  elocv  20214  isobs  20266  islinds  20350  scmatval  20512  fncld  21028  cnfval  21239  cnpval  21242  iscnp2  21245  1stcfb  21450  kgenf  21546  xkoopn  21594  dfac14  21623  hmeofn  21762  hmeofval  21763  filunirn  21887  alexsubALTlem2  22053  ucnval  22282  iscfilu  22293  ispsmet  22310  ismet  22329  isxmet  22330  xmetunirn  22343  cncfval  22892  ishtpy  22972  isphtpy  22981  om1bas  23031  cfilfval  23262  caufval  23273  iscmet  23282  dyadmax  23566  vitalilem2  23577  vitalilem3  23578  vitalilem4  23579  itg2monolem1  23716  fncpn  23895  elcpn  23896  mdegleb  24023  mdeg0  24029  mdegaddle  24033  mdegvsca  24035  uc1pval  24098  mon1pval  24100  aannenlem1  24282  aannenlem2  24283  aannenlem3  24284  vmaval  25038  sqff1o  25107  musum  25116  0sgmppw  25122  dchrval  25158  dchrbas  25159  tglnfn  25641  tglnunirn  25642  tglngval  25645  israg  25791  iseqlg  25946  ttgitvval  25961  ebtwntg  26061  incistruhgr  26173  usgredgleordALT  26325  uvtxavalOLD  26488  vtxdun  26587  vtxdlfgrval  26591  vtxd0nedgb  26594  vtxdushgrfvedglem  26595  vtxdushgrfvedg  26596  vtxdusgr0edgnelALT  26602  1loopgrvd2  26609  usgrvd0nedg  26639  vtxdginducedm1lem4  26648  rusgrnumwrdl2  26692  ewlksfval  26707  wwlksn  26940  wspthsn  26952  iswwlksnon  26957  iswwlksnonOLD  26958  iswspthsnon  26961  iswspthsnonOLD  26962  wwlksnexthasheq  27021  rusgrnumwlkg  27099  clwlkclwwlken  27135  clwwlkn  27151  clwwlknOLD  27152  clwwlken  27181  clwlkssizeeq  27229  clwlkssizeeqOLD  27230  clwwlknon  27235  clwwlknonOLD  27236  clwwlk0on0  27239  konigsberglem5  27408  fusgreg2wsplem  27487  fusgreghash2wsp  27492  2clwwlk  27504  numclwwlkovgOLD  27508  clwwlknonclwlknonen  27523  numclwlk1lem2  27531  numclwwlkovh0  27533  numclwwlkovq  27535  numclwwlkqhash  27536  numclwwlkovhOLD  27543  lnoval  27916  bloval  27945  hmoval  27974  ubthlem1  28035  ubthlem2  28036  ocval  28448  eigvecval  29064  specval  29066  rabfodom  29651  fpwrelmap  29817  locfinreflem  30216  ordtconnlem1  30279  sigaex  30481  isrnsigaOLD  30484  ddemeas  30608  ismbfm  30623  elunirnmbfm  30624  eulerpart  30753  ballotlem8  30907  reprval  30997  bnj110  31235  fncvm  31546  iscvm  31548  snmlval  31620  mpstval  31739  fvray  32554  icoreval  33512  fin2solem  33708  fin2so  33709  poimirlem4  33726  cnambfre  33771  istotbnd  33881  isbnd  33892  rngohomval  34076  rngoisoval  34089  idlval  34125  pridlval  34145  maxidlval  34151  lshpset  34768  lflset  34849  pats  35075  llnset  35294  lplnset  35318  lvolset  35361  isline  35528  pmapval  35546  paddval  35587  lhpset  35784  ldilset  35898  ltrnset  35907  dilsetN  35943  trnsetN  35946  diaval  36823  diafn  36825  lpolsetN  37273  lcdvadd  37388  lcdsca  37390  lcdvs  37394  mapdval  37419  mapd1o  37439  isnacs  37769  mzpclval  37790  pell1qrval  37912  pell14qrval  37914  pell1234qrval  37916  elmnc  38208  itgoval  38233  issdrg  38269  idomodle  38276  idomsubgmo  38278  k0004val  38950  icof  39910  elicores  40263  dvnprodlem1  40664  dvnprodlem2  40665  dvnprodlem3  40666  stoweidlem34  40754  fourierdlem2  40829  fourierdlem3  40830  etransclem12  40966  etransclem33  40987  ovnval2b  41272  volicorescl  41273  ovncvrrp  41284  ovnsubaddlem1  41290  ovncvr2  41331  issmflem  41442  smfaddlem1  41477  smfaddlem2  41478  smflimlem1  41485  fvmptrabdm  41817  iccpval  41861  ismgmhm  42293  issubmgm  42299  assintopval  42351  rnghmfn  42400  rnghmval  42401  isrngisom  42406  rngchomrnghmresALTV  42506  bigoval  42853  elbigofrcl  42854
  Copyright terms: Public domain W3C validator