Theorem rabex 5307

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

This proof depends on syntax axioms:   ∈ wcel 2147  {crab 3416  Vcvv 3454

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-in 4094  df-pw 4562

This theorem is used by:  rab2ex  5310  frminex  5637  ssimaex  7001  fvmptrabfv  7057  mptrabex  7262  fnpm  8892  inf3lema  9662  dfac2a  10247  kmlem1  10268  axcc4  10556  axdc3lem2  10568  axdc3lem4  10570  pwfseqlem1  10782  dfuzi  12830  uzval  13007  ixxval  13524  fzval  13681  bitsfval  16637  sadfval  16666  smufval  16691  phicl2  16989  hashgcdeq  17011  prmreclem4  17141  prmreclem5  17142  ismre  17810  fnmre  17811  mrisval  17854  isacs  17875  ismon  17958  isnat  18175  natffn  18177  initofn  18212  termofn  18213  initoval  18218  termoval  18219  coafval  18289  ismgmhm  18935  issubmgm  18941  ismhm  19030  issubm  19048  issubg  19386  isnsg  19415  gimfn  19525  isgim  19526  isga  19556  cntzval  19586  odfval  19797  odngen  19842  gexval  19843  isslw  19873  ablfac1a  20336  ablfac1b  20337  ablfac1c  20338  ablfac1eu  20340  ablfaclem1  20352  ablfaclem2  20353  ablfaclem3  20354  isirred  20700  rnghmfn  20720  rnghmval  20721  isrngim  20726  rhmval0  20756  isrim0  20764  rimfn  20788  issubrng  20850  issubrg  20874  rrgval  21000  issdrg  21096  abvfval  21118  lssset  21259  lmimfn  21352  islmhm  21353  islmim  21388  islbs  21402  ocvval  22028  elocv  22029  isobs  22081  islinds  22170  psrval  22278  psraddcl  22302  psrvscacl  22314  psrgrp  22319  psrlmod  22322  subrgpsr  22340  mvrf  22347  mplsubrg  22367  mplmonmul  22400  mplbas2  22406  opsrval  22410  rhmcomulmpl  22488  mhpval  22515  mhpmulcl  22525  mhpinvcl  22528  psdcl  22537  psdmplcl  22538  psdadd  22539  psdmul  22542  psrplusgpropd  22608  psropprmul  22610  scmatval  22874  fncld  23395  cnfval  23606  cnpval  23609  iscnp2  23612  1stcfb  23818  kgenf  23915  xkoopn  23963  dfac14  23992  hmeofn  24131  hmeofval  24132  filunirn  24256  alexsubALTlem2  24422  ucnval  24650  iscfilu  24661  ispsmet  24678  ismet  24697  isxmet  24698  xmetunirn  24711  cncfval  25264  ishtpy  25348  isphtpy  25357  om1bas  25407  cfilfval  25640  caufval  25651  iscmet  25660  dyadmax  25974  vitalilem2  25985  vitalilem3  25986  vitalilem4  25987  itg2monolem1  26126  fncpn  26308  elcpn  26309  mdeg0  26443  mdegaddle  26447  mdegvsca  26449  uc1pval  26513  mon1pval  26515  aannenlem1  26712  aannenlem2  26713  aannenlem3  26714  vmaval  27497  sqff1o  27566  musum  27575  dchrval  27618  dchrbas  27619  leftval  28292  rightval  28293  leftf  28298  rightf  28299  precsexlem4  28653  precsexlem5  28654  tglnfn  29067  tglnunirn  29068  tglngval  29071  israg  29229  tgplnfn  29310  isplng  29313  iseqlg  29469  ttgitvval  29516  ebtwntg  29617  incistruhgr  29714  usgredgleordALT  29872  vtxdun  30119  vtxdlfgrval  30123  vtxd0nedgb  30126  vtxdushgrfvedglem  30127  vtxdushgrfvedg  30128  vtxdusgr0edgnelALT  30134  1loopgrvd2  30141  usgrvd0nedg  30171  rusgrnumwrdl2  30224  ewlksfval  30239  wwlksn  30483  wspthsn  30494  iswwlksnon  30499  iswspthsnon  30502  wlknwwlksnen  30535  wwlksnexthasheq  30549  rusgrnumwlkg  30626  clwlkclwwlken  30660  clwwlkn  30674  clwwlken  30700  clwlkssizeeq  30733  clwwlknon  30738  clwwlk0on0  30740  konigsberglem5  30914  fusgreg2wsplem  30991  fusgreghash2wsp  30996  2clwwlk  31005  clwwlknonclwlknonen  31021  numclwlk1lem2  31028  numclwwlkovh0  31030  numclwwlkovq  31032  numclwwlkqhash  31033  lnoval  31411  bloval  31440  hmoval  31469  ubthlem1  31529  ubthlem2  31530  ocval  31939  eigvecval  32555  specval  32557  rabfodom  33200  fpwrelmap  33421  nsgmgc  34067  mxidlval  34090  ssmxidl  34103  rprmval  34152  selvply1rhmlem4  34266  evlextv  34285  mplvrpmfgalem  34287  mplvrpmga  34288  mplvrpmmhm  34289  mplvrpmrhm  34290  psrmonmul  34293  esplyfval0  34307  esplyfvaln  34317  locfinreflem  34583  rspectopn  34610  zarcls1  34612  zarclsun  34613  zarclsiin  34614  zarclsint  34615  zarclssn  34616  zarcls  34617  zartopn  34618  zar0ring  34621  zart0  34622  zarmxt1  34623  zarcmplem  34624  rhmpreimacnlem  34627  rhmpreimacn  34628  ordtconnlem1  34667  sigaex  34853  ddemeas  34980  ismbfm  34995  elunirnmbfm  34996  eulerpart  35125  ballotlem8  35280  reprval  35350  bnj110  35599  fncvm  36230  iscvm  36232  snmlval  36304  satfv1  36336  satfdm  36342  satffunlem1lem2  36376  satfv0fvfmla0  36386  satfv1fvfmla1  36396  mpstval  36508  fvray  37121  regsfromregtco  37541  icoreval  38544  fin2solem  38797  fin2so  38798  poimirlem4  38810  cnambfre  38854  istotbnd  38969  isbnd  38980  rngohomval  39164  rngoisoval  39177  idlval  39213  pridlval  39233  maxidlval  39239  lshpset  40301  lflset  40382  pats  40608  llnset  40828  lplnset  40852  lvolset  40895  isline  41062  pmapval  41080  paddval  41121  lhpset  41318  ldilset  41432  ltrnset  41441  dilsetN  41476  trnsetN  41479  diaval  42355  diafn  42357  lpolsetN  42805  lcdvadd  42920  lcdsca  42922  lcdvs  42926  mapdval  42951  mapd1o  42971  unitscyglem5  43515  psrmnd  43873  mhmcopsr  43874  mhmcoaddpsr  43875  rhmcomulpsr  43876  evlselv  43883  mhphf  43891  prjcrvval  43934  isnacs  43981  mzpclval  44002  pell1qrval  44119  pell14qrval  44121  pell1234qrval  44123  elmnc  44403  itgoval  44428  idomodle  44454  idomsubgmo  44456  k0004val  45411  permaxsep  46261  icof  46505  elicores  46818  dvnprodlem1  47229  dvnprodlem2  47230  dvnprodlem3  47231  stoweidlem34  47317  fourierdlem2  47392  fourierdlem3  47393  etransclem12  47529  etransclem33  47550  ovnval2b  47835  volicorescl  47836  ovncvrrp  47847  ovnsubaddlem1  47853  ovncvr2  47894  issmflem  48010  smfaddlem1  48046  smfaddlem2  48047  smflimlem1  48054  fvmptrabdm  48636  iccpval  48770  fppr  49097  grtri  49311  assintopval  49575  rngchomrnghmresALTV  49649  lazval  49725  bigoval  49992  elbigofrcl  49993  line  50176  rrxline  50178  sphere  50190  rrxsphere  50191