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

Theorem rabex 4773
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 4772 . 2 (𝐴 ∈ V → {𝑥𝐴𝜑} ∈ V)
31, 2ax-mp 5 1 {𝑥𝐴𝜑} ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 1987  {crab 2911  Vcvv 3186
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2916  df-v 3188  df-in 3562  df-ss 3569
This theorem is referenced by:  rab2ex  4776  rab2exOLD  4778  frminex  5054  ssimaex  6220  mptrabex  6442  mptrabexOLD  6443  fnpm  7810  inf3lema  8465  dfac2a  8896  kmlem1  8916  axcc4  9205  axdc3lem2  9217  axdc3lem4  9219  pwfseqlem1  9424  dfuzi  11412  uzval  11633  ixxval  12125  fzval  12270  bitsfval  15069  sadfval  15098  smufval  15123  phicl2  15397  hashgcdeq  15418  prmreclem4  15547  prmreclem5  15548  ismre  16171  fnmre  16172  mrisval  16211  isacs  16233  ismon  16314  isnat  16528  natffn  16530  initoval  16568  termoval  16569  coafval  16635  ismhm  17258  issubm  17268  issubg  17515  isnsg  17544  gimfn  17624  isgim  17625  isga  17645  cntzval  17675  odngen  17913  gexval  17914  isslw  17944  ablfac1a  18389  ablfac1b  18390  ablfac1c  18391  ablfac1eu  18393  ablfaclem1  18405  ablfaclem2  18406  ablfaclem3  18407  isirred  18620  isrim0  18644  issubrg  18701  abvfval  18739  lssset  18853  lmimfn  18945  islmhm  18946  islmim  18981  islbs  18995  rrgval  19206  psrval  19281  psraddcl  19302  psrvscacl  19312  psrgrp  19317  psrlmod  19320  subrgpsr  19338  mvrf  19343  mplsubrg  19359  mplmonmul  19383  mplbas2  19389  opsrval  19393  psrplusgpropd  19525  psropprmul  19527  ocvval  19930  elocv  19931  isobs  19983  islinds  20067  scmatval  20229  fncld  20736  cnfval  20947  cnpval  20950  iscnp2  20953  1stcfb  21158  kgenf  21254  xkoopn  21302  dfac14  21331  hmeofn  21470  hmeofval  21471  filunirn  21596  alexsubALTlem2  21762  ucnval  21991  iscfilu  22002  ispsmet  22019  ismet  22038  isxmet  22039  xmetunirn  22052  cncfval  22599  ishtpy  22679  isphtpy  22688  om1bas  22739  cfilfval  22970  caufval  22981  iscmet  22990  dyadmax  23272  vitalilem2  23284  vitalilem3  23285  vitalilem4  23286  itg2monolem1  23423  fncpn  23602  elcpn  23603  mdegleb  23728  mdeg0  23734  mdegaddle  23738  mdegvsca  23740  uc1pval  23803  mon1pval  23805  aannenlem1  23987  aannenlem2  23988  aannenlem3  23989  vmaval  24739  sqff1o  24808  musum  24817  0sgmppw  24823  dchrval  24859  dchrbas  24860  tglnfn  25342  tglnunirn  25343  tglngval  25346  israg  25492  iseqlg  25647  ttgitvval  25662  ebtwntg  25762  incistruhgr  25870  usgredgleordALT  26019  uvtxaval  26174  vtxdun  26263  vtxdlfgrval  26267  vtxd0nedgb  26270  vtxdushgrfvedglem  26271  vtxdushgrfvedg  26272  vtxdusgr0edgnelALT  26278  1loopgrvd2  26285  usgrvd0nedg  26315  rusgrnumwrdl2  26352  ewlksfval  26367  wwlksn  26598  wspthsn  26604  iswwlksnon  26609  iswspthsnon  26610  wwlksnexthasheq  26667  wwlks2onv  26716  rusgrnumwlkg  26739  clwwlksn  26748  clwlkssizeeq  26837  konigsberglem5  26984  fusgr2wsp2nb  27056  fusgreg2wsp  27058  2wspmdisj  27059  fusgreghash2wsp  27060  numclwwlkovf  27069  numclwwlkovg  27076  numclwwlkovq  27087  numclwwlkqhash  27088  numclwwlkovh  27089  lnoval  27456  bloval  27485  hmoval  27514  ubthlem1  27575  ubthlem2  27576  ocval  27988  eigvecval  28604  specval  28606  rabfodom  29191  fpwrelmap  29351  locfinreflem  29689  ordtconnlem1  29752  sigaex  29953  isrnsigaOLD  29956  ddemeas  30080  ismbfm  30095  elunirnmbfm  30096  eulerpart  30225  ballotlem8  30379  bnj110  30636  fncvm  30947  iscvm  30949  snmlval  31021  mpstval  31140  fvray  31890  icoreval  32833  fin2solem  33027  fin2so  33028  poimirlem4  33045  cnambfre  33090  istotbnd  33200  isbnd  33211  rngohomval  33395  rngoisoval  33408  idlval  33444  pridlval  33464  maxidlval  33470  lshpset  33745  lflset  33826  pats  34052  llnset  34271  lplnset  34295  lvolset  34338  isline  34505  pmapval  34523  paddval  34564  lhpset  34761  ldilset  34875  ltrnset  34884  dilsetN  34920  trnsetN  34923  diaval  35801  diafn  35803  lpolsetN  36251  lcdvadd  36366  lcdsca  36368  lcdvs  36372  mapdval  36397  mapd1o  36417  isnacs  36747  mzpclval  36768  pell1qrval  36890  pell14qrval  36892  pell1234qrval  36894  elmnc  37187  itgoval  37212  issdrg  37248  idomodle  37255  idomsubgmo  37257  k0004val  37930  icof  38885  elicores  39171  dvnprodlem1  39467  dvnprodlem2  39468  dvnprodlem3  39469  stoweidlem34  39558  fourierdlem2  39633  fourierdlem3  39634  etransclem12  39770  etransclem33  39791  ovnval2b  40073  volicorescl  40074  ovncvrrp  40085  ovnsubaddlem1  40091  ovncvr2  40132  issmflem  40243  smfaddlem1  40278  smfaddlem2  40279  smflimlem1  40286  iccpval  40649  ismgmhm  41071  issubmgm  41077  assintopval  41129  rnghmfn  41178  rnghmval  41179  isrngisom  41184  rngchomrnghmresALTV  41284  bigoval  41635  elbigofrcl  41636
  Copyright terms: Public domain W3C validator