Theorem rabex 5267

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

Step	Hyp	Ref	Expression
1		rabex.1	. 2 ⊢ 𝐴 ∈ V
2		rabexg 5265	. 2 ⊢ (𝐴 ∈ V → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)
3	1, 2	ax-mp 5	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V

Syntax hints:   ∈ wcel 2119  {crab 3391  Vcvv 3431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-in 3890  df-ss 3900  df-pw 4531

This theorem is referenced by:  rab2ex  5270  frminex  5597  ssimaex  6912  fvmptrabfv  6968  mptrabex  7169  fnpm  8771  inf3lema  9536  dfac2a  10043  kmlem1  10064  axcc4  10352  axdc3lem2  10364  axdc3lem4  10366  pwfseqlem1  10572  dfuzi  12611  uzval  12781  ixxval  13297  fzval  13454  bitsfval  16383  sadfval  16412  smufval  16437  phicl2  16729  hashgcdeq  16751  prmreclem4  16881  prmreclem5  16882  ismre  17543  fnmre  17544  mrisval  17587  isacs  17608  ismon  17691  isnat  17908  natffn  17910  initofn  17945  termofn  17946  initoval  17951  termoval  17952  coafval  18022  ismgmhm  18655  issubmgm  18661  ismhm  18744  issubm  18762  issubg  19093  isnsg  19121  gimfn  19227  isgim  19228  isga  19257  cntzval  19287  odfval  19498  odngen  19543  gexval  19544  isslw  19574  ablfac1a  20037  ablfac1b  20038  ablfac1c  20039  ablfac1eu  20041  ablfaclem1  20053  ablfaclem2  20054  ablfaclem3  20055  isirred  20390  rnghmfn  20410  rnghmval  20411  isrngim  20416  isrim0  20453  issubrng  20519  issubrg  20543  rrgval  20669  issdrg  20760  abvfval  20782  lssset  20923  lmimfn  21016  islmhm  21017  islmim  21052  islbs  21066  ocvval  21642  elocv  21643  isobs  21695  islinds  21784  psrval  21890  psraddcl  21914  psrvscacl  21926  psrgrp  21931  psrlmod  21934  subrgpsr  21952  mvrf  21959  mplsubrg  21979  mplmonmul  22012  mplbas2  22018  opsrval  22022  rhmcomulmpl  22100  mhpval  22127  mhpmulcl  22137  mhpinvcl  22140  psdcl  22149  psdmplcl  22150  psdadd  22151  psdmul  22154  psrplusgpropd  22220  psropprmul  22222  scmatval  22487  fncld  23005  cnfval  23216  cnpval  23219  iscnp2  23222  1stcfb  23428  kgenf  23524  xkoopn  23572  dfac14  23601  hmeofn  23740  hmeofval  23741  filunirn  23865  alexsubALTlem2  24031  ucnval  24259  iscfilu  24270  ispsmet  24287  ismet  24306  isxmet  24307  xmetunirn  24320  cncfval  24873  ishtpy  24957  isphtpy  24966  om1bas  25016  cfilfval  25249  caufval  25260  iscmet  25269  dyadmax  25583  vitalilem2  25594  vitalilem3  25595  vitalilem4  25596  itg2monolem1  25735  fncpn  25918  elcpn  25919  mdeg0  26053  mdegaddle  26057  mdegvsca  26059  uc1pval  26123  mon1pval  26125  aannenlem1  26312  aannenlem2  26313  aannenlem3  26314  vmaval  27094  sqff1o  27163  musum  27172  dchrval  27215  dchrbas  27216  leftval  27859  rightval  27860  leftf  27865  rightf  27866  precsexlem4  28220  precsexlem5  28221  tglnfn  28633  tglnunirn  28634  tglngval  28637  israg  28783  iseqlg  28953  ttgitvval  28968  ebtwntg  29069  incistruhgr  29166  usgredgleordALT  29321  vtxdun  29568  vtxdlfgrval  29572  vtxd0nedgb  29575  vtxdushgrfvedglem  29576  vtxdushgrfvedg  29577  vtxdusgr0edgnelALT  29583  1loopgrvd2  29590  usgrvd0nedg  29620  rusgrnumwrdl2  29673  ewlksfval  29688  wwlksn  29923  wspthsn  29934  iswwlksnon  29939  iswspthsnon  29942  wlknwwlksnen  29975  wwlksnexthasheq  29989  rusgrnumwlkg  30066  clwlkclwwlken  30100  clwwlkn  30114  clwwlken  30140  clwlkssizeeq  30173  clwwlknon  30178  clwwlk0on0  30180  konigsberglem5  30344  fusgreg2wsplem  30421  fusgreghash2wsp  30426  2clwwlk  30435  clwwlknonclwlknonen  30451  numclwlk1lem2  30458  numclwwlkovh0  30460  numclwwlkovq  30462  numclwwlkqhash  30463  lnoval  30841  bloval  30870  hmoval  30899  ubthlem1  30959  ubthlem2  30960  ocval  31369  eigvecval  31985  specval  31987  rabfodom  32593  fpwrelmap  32825  nsgmgc  33495  mxidlval  33544  ssmxidl  33557  rprmval  33599  selvply1rhmlem4  33707  evlextv  33726  mplvrpmfgalem  33728  mplvrpmga  33729  mplvrpmmhm  33730  mplvrpmrhm  33731  psrmonmul  33734  esplyfval0  33748  esplyfvaln  33758  locfinreflem  34024  rspectopn  34051  zarcls1  34053  zarclsun  34054  zarclsiin  34055  zarclsint  34056  zarclssn  34057  zarcls  34058  zartopn  34059  zar0ring  34062  zart0  34063  zarmxt1  34064  zarcmplem  34065  rhmpreimacnlem  34068  rhmpreimacn  34069  ordtconnlem1  34108  sigaex  34294  ddemeas  34420  ismbfm  34435  elunirnmbfm  34436  eulerpart  34566  ballotlem8  34721  reprval  34794  bnj110  35040  fncvm  35485  iscvm  35487  snmlval  35559  satfv1  35591  satfdm  35597  satffunlem1lem2  35631  satfv0fvfmla0  35641  satfv1fvfmla1  35651  mpstval  35763  fvray  36369  regsfromregtco  36766  icoreval  37715  fin2solem  37973  fin2so  37974  poimirlem4  37991  cnambfre  38035  istotbnd  38136  isbnd  38147  rngohomval  38331  rngoisoval  38344  idlval  38380  pridlval  38400  maxidlval  38406  lshpset  39470  lflset  39551  pats  39777  llnset  39997  lplnset  40021  lvolset  40064  isline  40231  pmapval  40249  paddval  40290  lhpset  40487  ldilset  40601  ltrnset  40610  dilsetN  40645  trnsetN  40648  diaval  41524  diafn  41526  lpolsetN  41974  lcdvadd  42089  lcdsca  42091  lcdvs  42095  mapdval  42120  mapd1o  42140  unitscyglem5  42684  psrmnd  43029  mhmcopsr  43030  mhmcoaddpsr  43031  rhmcomulpsr  43032  evlselv  43039  mhphf  43047  prjcrvval  43082  isnacs  43153  mzpclval  43174  pell1qrval  43291  pell14qrval  43293  pell1234qrval  43295  elmnc  43581  itgoval  43606  idomodle  43636  idomsubgmo  43638  k0004val  44594  permaxsep  45451  icof  45664  elicores  45978  dvnprodlem1  46389  dvnprodlem2  46390  dvnprodlem3  46391  stoweidlem34  46477  fourierdlem2  46552  fourierdlem3  46553  etransclem12  46689  etransclem33  46710  ovnval2b  46995  volicorescl  46996  ovncvrrp  47007  ovnsubaddlem1  47013  ovncvr2  47054  issmflem  47170  smfaddlem1  47206  smfaddlem2  47207  smflimlem1  47214  fvmptrabdm  47756  iccpval  47890  fppr  48217  grtri  48431  assintopval  48696  rngchomrnghmresALTV  48770  bigoval  49040  elbigofrcl  49041  line  49223  rrxline  49225  sphere  49238  rrxsphere  49239