Theorem rabex 5286

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 5284	. 2 ⊢ (𝐴 ∈ V → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)
3	1, 2	ax-mp 5	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V

Syntax hints:   ∈ wcel 2114  {crab 3401  Vcvv 3442

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-in 3910  df-ss 3920  df-pw 4558

This theorem is referenced by:  rab2ex  5289  frminex  5611  ssimaex  6927  fvmptrabfv  6982  mptrabex  7181  fnpm  8783  inf3lema  9545  dfac2a  10052  kmlem1  10073  axcc4  10361  axdc3lem2  10373  axdc3lem4  10375  pwfseqlem1  10581  dfuzi  12595  uzval  12765  ixxval  13281  fzval  13437  bitsfval  16362  sadfval  16391  smufval  16416  phicl2  16707  hashgcdeq  16729  prmreclem4  16859  prmreclem5  16860  ismre  17521  fnmre  17522  mrisval  17565  isacs  17586  ismon  17669  isnat  17886  natffn  17888  initofn  17923  termofn  17924  initoval  17929  termoval  17930  coafval  18000  ismgmhm  18633  issubmgm  18639  ismhm  18722  issubm  18740  issubg  19068  isnsg  19096  gimfn  19202  isgim  19203  isga  19232  cntzval  19262  odfval  19473  odngen  19518  gexval  19519  isslw  19549  ablfac1a  20012  ablfac1b  20013  ablfac1c  20014  ablfac1eu  20016  ablfaclem1  20028  ablfaclem2  20029  ablfaclem3  20030  isirred  20367  rnghmfn  20387  rnghmval  20388  isrngim  20393  isrim0  20430  issubrng  20492  issubrg  20516  rrgval  20642  issdrg  20733  abvfval  20755  lssset  20896  lmimfn  20990  islmhm  20991  islmim  21026  islbs  21040  ocvval  21634  elocv  21635  isobs  21687  islinds  21776  psrval  21883  psraddcl  21906  psraddclOLD  21907  psrvscacl  21919  psrgrp  21924  psrlmod  21927  subrgpsr  21945  mvrf  21952  mplsubrg  21972  mplmonmul  22003  mplbas2  22009  opsrval  22013  mhpval  22094  mhpmulcl  22104  mhpinvcl  22107  psdcl  22116  psdmplcl  22117  psdadd  22118  psdmul  22121  psrplusgpropd  22188  psropprmul  22190  rhmcomulmpl  22338  scmatval  22460  fncld  22978  cnfval  23189  cnpval  23192  iscnp2  23195  1stcfb  23401  kgenf  23497  xkoopn  23545  dfac14  23574  hmeofn  23713  hmeofval  23714  filunirn  23838  alexsubALTlem2  24004  ucnval  24232  iscfilu  24243  ispsmet  24260  ismet  24279  isxmet  24280  xmetunirn  24293  cncfval  24849  ishtpy  24939  isphtpy  24948  om1bas  24999  cfilfval  25232  caufval  25243  iscmet  25252  dyadmax  25567  vitalilem2  25578  vitalilem3  25579  vitalilem4  25580  itg2monolem1  25719  fncpn  25903  elcpn  25904  mdeg0  26043  mdegaddle  26047  mdegvsca  26049  uc1pval  26113  mon1pval  26115  aannenlem1  26304  aannenlem2  26305  aannenlem3  26306  vmaval  27091  sqff1o  27160  musum  27169  dchrval  27213  dchrbas  27214  leftval  27857  rightval  27858  leftf  27863  rightf  27864  precsexlem4  28218  precsexlem5  28219  tglnfn  28631  tglnunirn  28632  tglngval  28635  israg  28781  iseqlg  28951  ttgitvval  28966  ebtwntg  29067  incistruhgr  29164  usgredgleordALT  29319  vtxdun  29567  vtxdlfgrval  29571  vtxd0nedgb  29574  vtxdushgrfvedglem  29575  vtxdushgrfvedg  29576  vtxdusgr0edgnelALT  29582  1loopgrvd2  29589  usgrvd0nedg  29619  rusgrnumwrdl2  29672  ewlksfval  29687  wwlksn  29922  wspthsn  29933  iswwlksnon  29938  iswspthsnon  29941  wlknwwlksnen  29974  wwlksnexthasheq  29988  rusgrnumwlkg  30065  clwlkclwwlken  30099  clwwlkn  30113  clwwlken  30139  clwlkssizeeq  30172  clwwlknon  30177  clwwlk0on0  30179  konigsberglem5  30343  fusgreg2wsplem  30420  fusgreghash2wsp  30425  2clwwlk  30434  clwwlknonclwlknonen  30450  numclwlk1lem2  30457  numclwwlkovh0  30459  numclwwlkovq  30461  numclwwlkqhash  30462  lnoval  30840  bloval  30869  hmoval  30898  ubthlem1  30958  ubthlem2  30959  ocval  31368  eigvecval  31984  specval  31986  rabfodom  32592  fpwrelmap  32823  nsgmgc  33505  mxidlval  33554  ssmxidl  33567  rprmval  33609  evlextv  33719  mplvrpmfgalem  33721  mplvrpmga  33722  mplvrpmmhm  33723  mplvrpmrhm  33724  psrmonmul  33727  esplyfval0  33741  esplyfvaln  33751  locfinreflem  34018  rspectopn  34045  zarcls1  34047  zarclsun  34048  zarclsiin  34049  zarclsint  34050  zarclssn  34051  zarcls  34052  zartopn  34053  zar0ring  34056  zart0  34057  zarmxt1  34058  zarcmplem  34059  rhmpreimacnlem  34062  rhmpreimacn  34063  ordtconnlem1  34102  sigaex  34288  ddemeas  34414  ismbfm  34429  elunirnmbfm  34430  eulerpart  34560  ballotlem8  34715  reprval  34788  bnj110  35034  fncvm  35473  iscvm  35475  snmlval  35547  satfv1  35579  satfdm  35585  satffunlem1lem2  35619  satfv0fvfmla0  35629  satfv1fvfmla1  35639  mpstval  35751  fvray  36357  regsfromregtr  36690  icoreval  37608  fin2solem  37857  fin2so  37858  poimirlem4  37875  cnambfre  37919  istotbnd  38020  isbnd  38031  rngohomval  38215  rngoisoval  38228  idlval  38264  pridlval  38284  maxidlval  38290  lshpset  39354  lflset  39435  pats  39661  llnset  39881  lplnset  39905  lvolset  39948  isline  40115  pmapval  40133  paddval  40174  lhpset  40371  ldilset  40485  ltrnset  40494  dilsetN  40529  trnsetN  40532  diaval  41408  diafn  41410  lpolsetN  41858  lcdvadd  41973  lcdsca  41975  lcdvs  41979  mapdval  42004  mapd1o  42024  unitscyglem5  42569  psrmnd  42913  mhmcopsr  42917  mhmcoaddpsr  42918  rhmcomulpsr  42919  evlselv  42945  mhphf  42955  prjcrvval  42990  isnacs  43061  mzpclval  43082  pell1qrval  43203  pell14qrval  43205  pell1234qrval  43207  elmnc  43493  itgoval  43518  idomodle  43548  idomsubgmo  43550  k0004val  44506  permaxsep  45363  icof  45577  elicores  45893  dvnprodlem1  46304  dvnprodlem2  46305  dvnprodlem3  46306  stoweidlem34  46392  fourierdlem2  46467  fourierdlem3  46468  etransclem12  46604  etransclem33  46625  ovnval2b  46910  volicorescl  46911  ovncvrrp  46922  ovnsubaddlem1  46928  ovncvr2  46969  issmflem  47085  smfaddlem1  47121  smfaddlem2  47122  smflimlem1  47129  fvmptrabdm  47653  iccpval  47775  fppr  48086  grtri  48300  assintopval  48565  rngchomrnghmresALTV  48639  bigoval  48909  elbigofrcl  48910  line  49092  rrxline  49094  sphere  49107  rrxsphere  49108