Theorem rabex 5344

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

Syntax hints:   ∈ wcel 2105  {crab 3432  Vcvv 3477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-in 3969  df-ss 3979  df-pw 4606

This theorem is referenced by:  rab2ex  5347  frminex  5667  ssimaex  6993  fvmptrabfv  7047  mptrabex  7244  fnpm  8872  inf3lema  9661  dfac2a  10167  kmlem1  10188  axcc4  10476  axdc3lem2  10488  axdc3lem4  10490  pwfseqlem1  10695  dfuzi  12706  uzval  12877  ixxval  13391  fzval  13545  bitsfval  16456  sadfval  16485  smufval  16510  phicl2  16801  hashgcdeq  16822  prmreclem4  16952  prmreclem5  16953  ismre  17634  fnmre  17635  mrisval  17674  isacs  17695  ismon  17780  isnat  18001  natffn  18003  initofn  18040  termofn  18041  initoval  18046  termoval  18047  coafval  18117  ismgmhm  18721  issubmgm  18727  ismhm  18810  issubm  18828  issubg  19156  isnsg  19185  gimfn  19291  isgim  19292  isga  19321  cntzval  19351  odfval  19564  odngen  19609  gexval  19610  isslw  19640  ablfac1a  20103  ablfac1b  20104  ablfac1c  20105  ablfac1eu  20107  ablfaclem1  20119  ablfaclem2  20120  ablfaclem3  20121  isirred  20435  rnghmfn  20455  rnghmval  20456  isrngim  20461  isrim0OLD  20497  isrim0  20499  issubrng  20563  issubrg  20587  rrgval  20713  issdrg  20805  abvfval  20827  lssset  20948  lmimfn  21042  islmhm  21043  islmim  21078  islbs  21092  ocvval  21702  elocv  21703  isobs  21757  islinds  21846  psrval  21952  psraddcl  21975  psraddclOLD  21976  psrvscacl  21988  psrgrp  21993  psrgrpOLD  21994  psrlmod  21997  subrgpsr  22015  mvrf  22022  mplsubrg  22042  mplmonmul  22071  mplbas2  22077  opsrval  22081  mhpval  22160  mhpmulcl  22170  mhpinvcl  22173  psdcl  22182  psdmplcl  22183  psdadd  22184  psdmul  22187  psrplusgpropd  22252  psropprmul  22254  rhmcomulmpl  22401  scmatval  22525  fncld  23045  cnfval  23256  cnpval  23259  iscnp2  23262  1stcfb  23468  kgenf  23564  xkoopn  23612  dfac14  23641  hmeofn  23780  hmeofval  23781  filunirn  23905  alexsubALTlem2  24071  ucnval  24301  iscfilu  24312  ispsmet  24329  ismet  24348  isxmet  24349  xmetunirn  24362  cncfval  24927  ishtpy  25017  isphtpy  25026  om1bas  25077  cfilfval  25311  caufval  25322  iscmet  25331  dyadmax  25646  vitalilem2  25657  vitalilem3  25658  vitalilem4  25659  itg2monolem1  25799  fncpn  25983  elcpn  25984  mdeg0  26123  mdegaddle  26127  mdegvsca  26129  uc1pval  26193  mon1pval  26195  aannenlem1  26384  aannenlem2  26385  aannenlem3  26386  vmaval  27170  sqff1o  27239  musum  27248  dchrval  27292  dchrbas  27293  leftval  27916  rightval  27917  leftf  27918  rightf  27919  precsexlem4  28248  precsexlem5  28249  tglnfn  28569  tglnunirn  28570  tglngval  28573  israg  28719  iseqlg  28889  ttgitvval  28910  ebtwntg  29011  incistruhgr  29110  usgredgleordALT  29265  vtxdun  29513  vtxdlfgrval  29517  vtxd0nedgb  29520  vtxdushgrfvedglem  29521  vtxdushgrfvedg  29522  vtxdusgr0edgnelALT  29528  1loopgrvd2  29535  usgrvd0nedg  29565  rusgrnumwrdl2  29618  ewlksfval  29633  wwlksn  29866  wspthsn  29877  iswwlksnon  29882  iswspthsnon  29885  wlknwwlksnen  29918  wwlksnexthasheq  29932  rusgrnumwlkg  30006  clwlkclwwlken  30040  clwwlkn  30054  clwwlken  30080  clwlkssizeeq  30113  clwwlknon  30118  clwwlk0on0  30120  konigsberglem5  30284  fusgreg2wsplem  30361  fusgreghash2wsp  30366  2clwwlk  30375  clwwlknonclwlknonen  30391  numclwlk1lem2  30398  numclwwlkovh0  30400  numclwwlkovq  30402  numclwwlkqhash  30403  lnoval  30780  bloval  30809  hmoval  30838  ubthlem1  30898  ubthlem2  30899  ocval  31308  eigvecval  31924  specval  31926  rabfodom  32532  fpwrelmap  32750  nsgmgc  33419  mxidlval  33468  ssmxidl  33481  rprmval  33523  locfinreflem  33800  rspectopn  33827  zarcls1  33829  zarclsun  33830  zarclsiin  33831  zarclsint  33832  zarclssn  33833  zarcls  33834  zartopn  33835  zar0ring  33838  zart0  33839  zarmxt1  33840  zarcmplem  33841  rhmpreimacnlem  33844  rhmpreimacn  33845  ordtconnlem1  33884  sigaex  34090  ddemeas  34216  ismbfm  34231  elunirnmbfm  34232  eulerpart  34363  ballotlem8  34517  reprval  34603  bnj110  34850  fncvm  35241  iscvm  35243  snmlval  35315  satfv1  35347  satfdm  35353  satffunlem1lem2  35387  satfv0fvfmla0  35397  satfv1fvfmla1  35407  mpstval  35519  fvray  36122  icoreval  37335  fin2solem  37592  fin2so  37593  poimirlem4  37610  cnambfre  37654  istotbnd  37755  isbnd  37766  rngohomval  37950  rngoisoval  37963  idlval  37999  pridlval  38019  maxidlval  38025  lshpset  38959  lflset  39040  pats  39266  llnset  39487  lplnset  39511  lvolset  39554  isline  39721  pmapval  39739  paddval  39780  lhpset  39977  ldilset  40091  ltrnset  40100  dilsetN  40135  trnsetN  40138  diaval  41014  diafn  41016  lpolsetN  41464  lcdvadd  41579  lcdsca  41581  lcdvs  41585  mapdval  41610  mapd1o  41630  unitscyglem5  42180  psrmnd  42531  mhmcopsr  42535  mhmcoaddpsr  42536  rhmcomulpsr  42537  evlselv  42573  mhphf  42583  prjcrvval  42618  isnacs  42691  mzpclval  42712  pell1qrval  42833  pell14qrval  42835  pell1234qrval  42837  elmnc  43124  itgoval  43149  idomodle  43179  idomsubgmo  43181  k0004val  44139  icof  45161  elicores  45485  dvnprodlem1  45901  dvnprodlem2  45902  dvnprodlem3  45903  stoweidlem34  45989  fourierdlem2  46064  fourierdlem3  46065  etransclem12  46201  etransclem33  46222  ovnval2b  46507  volicorescl  46508  ovncvrrp  46519  ovnsubaddlem1  46525  ovncvr2  46566  issmflem  46682  smfaddlem1  46718  smfaddlem2  46719  smflimlem1  46726  fvmptrabdm  47242  iccpval  47339  fppr  47650  grtri  47844  assintopval  48048  rngchomrnghmresALTV  48122  bigoval  48398  elbigofrcl  48399  line  48581  rrxline  48583  sphere  48596  rrxsphere  48597