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

Theorem rabex 4740
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 4739 . 2 (𝐴 ∈ V → {𝑥𝐴𝜑} ∈ V)
31, 2ax-mp 5 1 {𝑥𝐴𝜑} ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 1977  {crab 2900  Vcvv 3173
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-in 3547  df-ss 3554
This theorem is referenced by:  rab2ex  4743  rab2exOLD  4745  frminex  5018  ssimaex  6173  mptrabex  6392  mptrabexOLD  6393  fnpm  7752  inf3lema  8404  dfac2a  8835  kmlem1  8855  axcc4  9144  axdc3lem2  9156  axdc3lem4  9158  pwfseqlem1  9359  dfuzi  11344  uzval  11565  ixxval  12054  fzval  12199  bitsfval  14983  sadfval  15012  smufval  15037  phicl2  15311  hashgcdeq  15332  prmreclem4  15461  prmreclem5  15462  ismre  16073  fnmre  16074  mrisval  16113  isacs  16135  ismon  16216  isnat  16430  natffn  16432  initoval  16470  termoval  16471  coafval  16537  ismhm  17160  issubm  17170  issubg  17417  isnsg  17446  gimfn  17526  isgim  17527  isga  17547  cntzval  17577  odngen  17815  gexval  17816  isslw  17846  ablfac1a  18291  ablfac1b  18292  ablfac1c  18293  ablfac1eu  18295  ablfaclem1  18307  ablfaclem2  18308  ablfaclem3  18309  isirred  18522  isrim0  18546  issubrg  18603  abvfval  18641  lssset  18755  lmimfn  18847  islmhm  18848  islmim  18883  islbs  18897  rrgval  19108  psrval  19183  psraddcl  19204  psrvscacl  19214  psrgrp  19219  psrlmod  19222  subrgpsr  19240  mvrf  19245  mplsubrg  19261  mplmonmul  19285  mplbas2  19291  opsrval  19295  psrplusgpropd  19427  psropprmul  19429  ocvval  19830  elocv  19831  isobs  19883  islinds  19967  scmatval  20129  fncld  20636  cnfval  20847  cnpval  20850  iscnp2  20853  1stcfb  21058  kgenf  21154  xkoopn  21202  dfac14  21231  hmeofn  21370  hmeofval  21371  filunirn  21496  alexsubALTlem2  21662  ucnval  21891  iscfilu  21902  ispsmet  21919  ismet  21938  isxmet  21939  xmetunirn  21952  cncfval  22499  ishtpy  22579  isphtpy  22588  om1bas  22639  cfilfval  22870  caufval  22881  iscmet  22890  dyadmax  23172  vitalilem2  23184  vitalilem3  23185  vitalilem4  23186  itg2monolem1  23323  fncpn  23502  elcpn  23503  mdegleb  23628  mdeg0  23634  mdegaddle  23638  mdegvsca  23640  uc1pval  23703  mon1pval  23705  aannenlem1  23887  aannenlem2  23888  aannenlem3  23889  vmaval  24639  sqff1o  24708  musum  24717  0sgmppw  24723  dchrval  24759  dchrbas  24760  tglnfn  25242  tglnunirn  25243  tglngval  25246  israg  25392  iseqlg  25547  ttgitvval  25562  ebtwntg  25662  incistruhgr  25746  wwlkexthasheq  26262  clwlksizeeq  26379  rusgranumwlklem1  26476  rusgranumwlklem3  26478  rusgranumwlklem4  26479  rusgranumwwlkg  26486  numclwwlkovf  26608  numclwwlkovg  26614  numclwwlkovq  26626  numclwwlkqhash  26627  numclwwlkovh  26628  lnoval  26991  bloval  27020  hmoval  27049  ubthlem1  27110  ubthlem2  27111  ocval  27523  eigvecval  28139  specval  28141  rabfodom  28728  fpwrelmap  28896  locfinreflem  29235  ordtconlem1  29298  sigaex  29499  isrnsigaOLD  29502  ddemeas  29626  ismbfm  29641  elunirnmbfm  29642  eulerpart  29771  ballotlem8  29925  bnj110  30182  fncvm  30493  iscvm  30495  snmlval  30567  mpstval  30686  fvray  31418  icoreval  32377  fin2solem  32565  fin2so  32566  poimirlem4  32583  cnambfre  32628  istotbnd  32738  isbnd  32749  rngohomval  32933  rngoisoval  32946  idlval  32982  pridlval  33002  maxidlval  33008  lshpset  33283  lflset  33364  pats  33590  llnset  33809  lplnset  33833  lvolset  33876  isline  34043  pmapval  34061  paddval  34102  lhpset  34299  ldilset  34413  ltrnset  34422  dilsetN  34458  trnsetN  34461  diaval  35339  diafn  35341  lpolsetN  35789  lcdvadd  35904  lcdsca  35906  lcdvs  35910  mapdval  35935  mapd1o  35955  isnacs  36285  mzpclval  36306  pell1qrval  36428  pell14qrval  36430  pell1234qrval  36432  elmnc  36725  itgoval  36750  issdrg  36786  idomodle  36793  idomsubgmo  36795  k0004val  37468  icof  38406  elicores  38607  dvnprodlem1  38836  dvnprodlem2  38837  dvnprodlem3  38838  stoweidlem34  38927  fourierdlem2  39002  fourierdlem3  39003  etransclem12  39139  etransclem33  39160  ovnval2b  39442  volicorescl  39443  ovncvrrp  39454  ovnsubaddlem1  39460  ovncvr2  39501  issmflem  39613  smfaddlem1  39649  smfaddlem2  39650  smflimlem1  39657  iccpval  39953  usgredgaleordALT  40461  uvtxaval  40613  vtxdun  40696  vtxdlfgrval  40700  vtxd0nedgb  40703  vtxdushgrfvedglem  40704  vtxdushgrfvedg  40705  vtxdusgr0edgnelALT  40711  1loopgrvd2  40718  usgrvd0nedg  40749  rusgrnumwrdl2  40786  ewlksfval  40803  wwlksn  41040  wspthsn  41046  iswwlksnon  41051  iswspthsnon  41052  wwlksnexthasheq  41109  wwlks2onv  41158  rusgrnumwlkg  41180  clwwlksn  41189  clwlkssizeeq  41278  konigsberglem5  41426  fusgr2wsp2nb  41498  fusgreg2wsp  41500  2wspmdisj  41501  fusgreghash2wsp  41502  av-numclwwlkovf  41511  av-numclwwlkovg  41518  av-numclwwlkovq  41529  av-numclwwlkqhash  41530  av-numclwwlkovh  41531  ismgmhm  41573  issubmgm  41579  assintopval  41631  rnghmfn  41680  rnghmval  41681  isrngisom  41686  rngchomrnghmresALTV  41788  bigoval  42141  elbigofrcl  42142
  Copyright terms: Public domain W3C validator