Theorem rabex 5199

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

Syntax hints:   ∈ wcel 2111  {crab 3110  Vcvv 3441

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-sep 5167

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  rab2ex  5202  frminex  5499  ssimaex  6723  fvmptrabfv  6776  mptrabex  6965  fnpm  8397  inf3lema  9071  dfac2a  9540  kmlem1  9561  axcc4  9850  axdc3lem2  9862  axdc3lem4  9864  pwfseqlem1  10069  dfuzi  12061  uzval  12233  ixxval  12734  fzval  12887  bitsfval  15762  sadfval  15791  smufval  15816  phicl2  16095  hashgcdeq  16116  prmreclem4  16245  prmreclem5  16246  ismre  16853  fnmre  16854  mrisval  16893  isacs  16914  ismon  16995  isnat  17209  natffn  17211  initoval  17249  termoval  17250  coafval  17316  ismhm  17950  issubm  17960  issubg  18271  isnsg  18299  gimfn  18393  isgim  18394  isga  18413  cntzval  18443  odfval  18652  odngen  18694  gexval  18695  isslw  18725  ablfac1a  19184  ablfac1b  19185  ablfac1c  19186  ablfac1eu  19188  ablfaclem1  19200  ablfaclem2  19201  ablfaclem3  19202  isirred  19445  isrim0  19471  issubrg  19528  issdrg  19567  abvfval  19582  lssset  19698  lmimfn  19791  islmhm  19792  islmim  19827  islbs  19841  rrgval  20053  ocvval  20356  elocv  20357  isobs  20409  islinds  20498  psrval  20600  psraddcl  20621  psrvscacl  20631  psrgrp  20636  psrlmod  20639  subrgpsr  20657  mvrf  20662  mplsubrg  20678  mplmonmul  20704  mplbas2  20710  opsrval  20714  mhpval  20792  mhpvarcl  20798  mhpinvcl  20800  psrplusgpropd  20865  psropprmul  20867  scmatval  21109  fncld  21627  cnfval  21838  cnpval  21841  iscnp2  21844  1stcfb  22050  kgenf  22146  xkoopn  22194  dfac14  22223  hmeofn  22362  hmeofval  22363  filunirn  22487  alexsubALTlem2  22653  ucnval  22883  iscfilu  22894  ispsmet  22911  ismet  22930  isxmet  22931  xmetunirn  22944  cncfval  23493  ishtpy  23577  isphtpy  23586  om1bas  23636  cfilfval  23868  caufval  23879  iscmet  23888  dyadmax  24202  vitalilem2  24213  vitalilem3  24214  vitalilem4  24215  itg2monolem1  24354  fncpn  24536  elcpn  24537  mdegleb  24665  mdeg0  24671  mdegaddle  24675  mdegvsca  24677  uc1pval  24740  mon1pval  24742  aannenlem1  24924  aannenlem2  24925  aannenlem3  24926  vmaval  25698  sqff1o  25767  musum  25776  dchrval  25818  dchrbas  25819  tglnfn  26341  tglnunirn  26342  tglngval  26345  israg  26491  iseqlg  26661  ttgitvval  26676  ebtwntg  26776  incistruhgr  26872  usgredgleordALT  27024  vtxdun  27271  vtxdlfgrval  27275  vtxd0nedgb  27278  vtxdushgrfvedglem  27279  vtxdushgrfvedg  27280  vtxdusgr0edgnelALT  27286  1loopgrvd2  27293  usgrvd0nedg  27323  rusgrnumwrdl2  27376  ewlksfval  27391  wwlksn  27623  wspthsn  27634  iswwlksnon  27639  iswspthsnon  27642  wlknwwlksnen  27675  wwlksnexthasheq  27689  rusgrnumwlkg  27763  clwlkclwwlken  27797  clwwlkn  27811  clwwlken  27837  clwlkssizeeq  27870  clwwlknon  27875  clwwlk0on0  27877  konigsberglem5  28041  fusgreg2wsplem  28118  fusgreghash2wsp  28123  2clwwlk  28132  clwwlknonclwlknonen  28148  numclwlk1lem2  28155  numclwwlkovh0  28157  numclwwlkovq  28159  numclwwlkqhash  28160  lnoval  28535  bloval  28564  hmoval  28593  ubthlem1  28653  ubthlem2  28654  ocval  29063  eigvecval  29679  specval  29681  rabfodom  30274  fpwrelmap  30495  mxidlval  31041  ssmxidl  31050  rprmval  31072  locfinreflem  31193  rspectopn  31220  zarcls1  31222  zarclsun  31223  zarclsiin  31224  zarclsint  31225  zarclssn  31226  zarcls  31227  zartopn  31228  zar0ring  31231  zart0  31232  zarmxt1  31233  zarcmplem  31234  rhmpreimacnlem  31237  rhmpreimacn  31238  ordtconnlem1  31277  sigaex  31479  ddemeas  31605  ismbfm  31620  elunirnmbfm  31621  eulerpart  31750  ballotlem8  31904  reprval  31991  bnj110  32240  fncvm  32617  iscvm  32619  snmlval  32691  satfv1  32723  satfdm  32729  satffunlem1lem2  32763  satfv0fvfmla0  32773  satfv1fvfmla1  32783  mpstval  32895  fvray  33715  icoreval  34770  fin2solem  35043  fin2so  35044  poimirlem4  35061  cnambfre  35105  istotbnd  35207  isbnd  35218  rngohomval  35402  rngoisoval  35415  idlval  35451  pridlval  35471  maxidlval  35477  lshpset  36274  lflset  36355  pats  36581  llnset  36801  lplnset  36825  lvolset  36868  isline  37035  pmapval  37053  paddval  37094  lhpset  37291  ldilset  37405  ltrnset  37414  dilsetN  37449  trnsetN  37452  diaval  38328  diafn  38330  lpolsetN  38778  lcdvadd  38893  lcdsca  38895  lcdvs  38899  mapdval  38924  mapd1o  38944  selvval2lem4  39431  isnacs  39645  mzpclval  39666  pell1qrval  39787  pell14qrval  39789  pell1234qrval  39791  elmnc  40080  itgoval  40105  idomodle  40140  idomsubgmo  40142  k0004val  40853  icof  41848  elicores  42170  dvnprodlem1  42588  dvnprodlem2  42589  dvnprodlem3  42590  stoweidlem34  42676  fourierdlem2  42751  fourierdlem3  42752  etransclem12  42888  etransclem33  42909  ovnval2b  43191  volicorescl  43192  ovncvrrp  43203  ovnsubaddlem1  43209  ovncvr2  43250  issmflem  43361  smfaddlem1  43396  smfaddlem2  43397  smflimlem1  43404  fvmptrabdm  43849  iccpval  43932  fppr  44244  ismgmhm  44403  issubmgm  44409  assintopval  44465  rnghmfn  44514  rnghmval  44515  isrngisom  44520  rngchomrnghmresALTV  44620  bigoval  44963  elbigofrcl  44964  line  45146  rrxline  45148  sphere  45161  rrxsphere  45162