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

Theorem rabex 5211
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 5210 . 2 (𝐴 ∈ V → {𝑥𝐴𝜑} ∈ V)
31, 2ax-mp 5 1 {𝑥𝐴𝜑} ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2114  {crab 3134  Vcvv 3469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-rab 3139  df-v 3471  df-in 3915  df-ss 3925
This theorem is referenced by:  rab2ex  5214  frminex  5512  ssimaex  6730  fvmptrabfv  6781  mptrabex  6970  fnpm  8401  inf3lema  9075  dfac2a  9544  kmlem1  9565  axcc4  9850  axdc3lem2  9862  axdc3lem4  9864  pwfseqlem1  10069  dfuzi  12061  uzval  12233  ixxval  12734  fzval  12887  bitsfval  15761  sadfval  15790  smufval  15815  phicl2  16094  hashgcdeq  16115  prmreclem4  16244  prmreclem5  16245  ismre  16852  fnmre  16853  mrisval  16892  isacs  16913  ismon  16994  isnat  17208  natffn  17210  initoval  17248  termoval  17249  coafval  17315  ismhm  17949  issubm  17959  issubg  18270  isnsg  18298  gimfn  18392  isgim  18393  isga  18412  cntzval  18442  odfval  18651  odngen  18693  gexval  18694  isslw  18724  ablfac1a  19182  ablfac1b  19183  ablfac1c  19184  ablfac1eu  19186  ablfaclem1  19198  ablfaclem2  19199  ablfaclem3  19200  isirred  19443  isrim0  19469  issubrg  19526  issdrg  19565  abvfval  19580  lssset  19696  lmimfn  19789  islmhm  19790  islmim  19825  islbs  19839  rrgval  20051  ocvval  20354  elocv  20355  isobs  20407  islinds  20496  psrval  20598  psraddcl  20619  psrvscacl  20629  psrgrp  20634  psrlmod  20637  subrgpsr  20655  mvrf  20660  mplsubrg  20676  mplmonmul  20702  mplbas2  20708  opsrval  20712  mhpval  20790  mhpvarcl  20796  mhpinvcl  20798  psrplusgpropd  20863  psropprmul  20865  scmatval  21107  fncld  21625  cnfval  21836  cnpval  21839  iscnp2  21842  1stcfb  22048  kgenf  22144  xkoopn  22192  dfac14  22221  hmeofn  22360  hmeofval  22361  filunirn  22485  alexsubALTlem2  22651  ucnval  22881  iscfilu  22892  ispsmet  22909  ismet  22928  isxmet  22929  xmetunirn  22942  cncfval  23491  ishtpy  23575  isphtpy  23584  om1bas  23634  cfilfval  23866  caufval  23877  iscmet  23886  dyadmax  24200  vitalilem2  24211  vitalilem3  24212  vitalilem4  24213  itg2monolem1  24352  fncpn  24534  elcpn  24535  mdegleb  24663  mdeg0  24669  mdegaddle  24673  mdegvsca  24675  uc1pval  24738  mon1pval  24740  aannenlem1  24922  aannenlem2  24923  aannenlem3  24924  vmaval  25696  sqff1o  25765  musum  25774  dchrval  25816  dchrbas  25817  tglnfn  26339  tglnunirn  26340  tglngval  26343  israg  26489  iseqlg  26659  ttgitvval  26674  ebtwntg  26774  incistruhgr  26870  usgredgleordALT  27022  vtxdun  27269  vtxdlfgrval  27273  vtxd0nedgb  27276  vtxdushgrfvedglem  27277  vtxdushgrfvedg  27278  vtxdusgr0edgnelALT  27284  1loopgrvd2  27291  usgrvd0nedg  27321  rusgrnumwrdl2  27374  ewlksfval  27389  wwlksn  27621  wspthsn  27632  iswwlksnon  27637  iswspthsnon  27640  wlknwwlksnen  27673  wwlksnexthasheq  27687  rusgrnumwlkg  27761  clwlkclwwlken  27795  clwwlkn  27809  clwwlken  27835  clwlkssizeeq  27868  clwwlknon  27873  clwwlk0on0  27875  konigsberglem5  28039  fusgreg2wsplem  28116  fusgreghash2wsp  28121  2clwwlk  28130  clwwlknonclwlknonen  28146  numclwlk1lem2  28153  numclwwlkovh0  28155  numclwwlkovq  28157  numclwwlkqhash  28158  lnoval  28533  bloval  28562  hmoval  28591  ubthlem1  28651  ubthlem2  28652  ocval  29061  eigvecval  29677  specval  29679  rabfodom  30272  fpwrelmap  30479  mxidlval  31012  ssmxidl  31021  locfinreflem  31162  rspectopn  31189  zarcls1  31191  zarclsun  31192  zarclsiin  31193  zarclsint  31194  zarclssn  31195  zarcls  31196  zartopn  31197  zart0  31200  zarmxt1  31201  ordtconnlem1  31241  sigaex  31443  ddemeas  31569  ismbfm  31584  elunirnmbfm  31585  eulerpart  31714  ballotlem8  31868  reprval  31955  bnj110  32204  fncvm  32578  iscvm  32580  snmlval  32652  satfv1  32684  satfdm  32690  satffunlem1lem2  32724  satfv0fvfmla0  32734  satfv1fvfmla1  32744  mpstval  32856  fvray  33676  icoreval  34731  fin2solem  35001  fin2so  35002  poimirlem4  35019  cnambfre  35063  istotbnd  35165  isbnd  35176  rngohomval  35360  rngoisoval  35373  idlval  35409  pridlval  35429  maxidlval  35435  lshpset  36232  lflset  36313  pats  36539  llnset  36759  lplnset  36783  lvolset  36826  isline  36993  pmapval  37011  paddval  37052  lhpset  37249  ldilset  37363  ltrnset  37372  dilsetN  37407  trnsetN  37410  diaval  38286  diafn  38288  lpolsetN  38736  lcdvadd  38851  lcdsca  38853  lcdvs  38857  mapdval  38882  mapd1o  38902  selvval2lem4  39377  isnacs  39575  mzpclval  39596  pell1qrval  39717  pell14qrval  39719  pell1234qrval  39721  elmnc  40010  itgoval  40035  idomodle  40070  idomsubgmo  40072  k0004val  40786  icof  41786  elicores  42109  dvnprodlem1  42527  dvnprodlem2  42528  dvnprodlem3  42529  stoweidlem34  42615  fourierdlem2  42690  fourierdlem3  42691  etransclem12  42827  etransclem33  42848  ovnval2b  43130  volicorescl  43131  ovncvrrp  43142  ovnsubaddlem1  43148  ovncvr2  43189  issmflem  43300  smfaddlem1  43335  smfaddlem2  43336  smflimlem1  43343  fvmptrabdm  43788  iccpval  43871  fppr  44183  ismgmhm  44342  issubmgm  44348  assintopval  44404  rnghmfn  44453  rnghmval  44454  isrngisom  44459  rngchomrnghmresALTV  44559  bigoval  44902  elbigofrcl  44903  line  45085  rrxline  45087  sphere  45100  rrxsphere  45101
  Copyright terms: Public domain W3C validator