Theorem rabex 5295

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

Syntax hints:   ∈ wcel 2142  {crab 3414  Vcvv 3454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1100  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-in 3911  df-ss 3921  df-pw 4557

This theorem is referenced by:  rab2ex  5298  frminex  5626  ssimaex  6952  fvmptrabfv  7008  mptrabex  7209  fnpm  8815  inf3lema  9579  dfac2a  10086  kmlem1  10107  axcc4  10396  axdc3lem2  10408  axdc3lem4  10410  pwfseqlem1  10616  dfuzi  12664  uzval  12841  ixxval  13357  fzval  13514  bitsfval  16457  sadfval  16486  smufval  16511  phicl2  16803  hashgcdeq  16825  prmreclem4  16955  prmreclem5  16956  ismre  17618  fnmre  17619  mrisval  17662  isacs  17683  ismon  17766  isnat  17983  natffn  17985  initofn  18020  termofn  18021  initoval  18026  termoval  18027  coafval  18097  ismgmhm  18730  issubmgm  18736  ismhm  18819  issubm  18837  issubg  19168  isnsg  19196  gimfn  19301  isgim  19302  isga  19331  cntzval  19361  odfval  19572  odngen  19617  gexval  19618  isslw  19648  ablfac1a  20111  ablfac1b  20112  ablfac1c  20113  ablfac1eu  20115  ablfaclem1  20127  ablfaclem2  20128  ablfaclem3  20129  isirred  20464  rnghmfn  20484  rnghmval  20485  isrngim  20490  isrim0  20527  issubrng  20593  issubrg  20617  rrgval  20743  issdrg  20834  abvfval  20856  lssset  20997  lmimfn  21090  islmhm  21091  islmim  21126  islbs  21140  ocvval  21716  elocv  21717  isobs  21769  islinds  21858  psrval  21964  psraddcl  21988  psrvscacl  22000  psrgrp  22005  psrlmod  22008  subrgpsr  22026  mvrf  22033  mplsubrg  22053  mplmonmul  22086  mplbas2  22092  opsrval  22096  rhmcomulmpl  22174  mhpval  22201  mhpmulcl  22211  mhpinvcl  22214  psdcl  22223  psdmplcl  22224  psdadd  22225  psdmul  22228  psrplusgpropd  22294  psropprmul  22296  scmatval  22561  fncld  23079  cnfval  23290  cnpval  23293  iscnp2  23296  1stcfb  23502  kgenf  23598  xkoopn  23646  dfac14  23675  hmeofn  23814  hmeofval  23815  filunirn  23939  alexsubALTlem2  24105  ucnval  24333  iscfilu  24344  ispsmet  24361  ismet  24380  isxmet  24381  xmetunirn  24394  cncfval  24947  ishtpy  25031  isphtpy  25040  om1bas  25090  cfilfval  25323  caufval  25334  iscmet  25343  dyadmax  25657  vitalilem2  25668  vitalilem3  25669  vitalilem4  25670  itg2monolem1  25809  fncpn  25992  elcpn  25993  mdeg0  26127  mdegaddle  26131  mdegvsca  26133  uc1pval  26197  mon1pval  26199  aannenlem1  26389  aannenlem2  26390  aannenlem3  26391  vmaval  27174  sqff1o  27243  musum  27252  dchrval  27295  dchrbas  27296  leftval  27939  rightval  27940  leftf  27945  rightf  27946  precsexlem4  28300  precsexlem5  28301  tglnfn  28713  tglnunirn  28714  tglngval  28717  israg  28867  tgplnfn  28979  isplng  28982  iseqlg  29058  ttgitvval  29079  ebtwntg  29180  incistruhgr  29277  usgredgleordALT  29432  vtxdun  29679  vtxdlfgrval  29683  vtxd0nedgb  29686  vtxdushgrfvedglem  29687  vtxdushgrfvedg  29688  vtxdusgr0edgnelALT  29694  1loopgrvd2  29701  usgrvd0nedg  29731  rusgrnumwrdl2  29784  ewlksfval  29799  wwlksn  30034  wspthsn  30045  iswwlksnon  30050  iswspthsnon  30053  wlknwwlksnen  30086  wwlksnexthasheq  30100  rusgrnumwlkg  30177  clwlkclwwlken  30211  clwwlkn  30225  clwwlken  30251  clwlkssizeeq  30284  clwwlknon  30289  clwwlk0on0  30291  konigsberglem5  30455  fusgreg2wsplem  30532  fusgreghash2wsp  30537  2clwwlk  30546  clwwlknonclwlknonen  30562  numclwlk1lem2  30569  numclwwlkovh0  30571  numclwwlkovq  30573  numclwwlkqhash  30574  lnoval  30952  bloval  30981  hmoval  31010  ubthlem1  31070  ubthlem2  31071  ocval  31480  eigvecval  32096  specval  32098  rabfodom  32701  fpwrelmap  32932  nsgmgc  33595  mxidlval  33646  ssmxidl  33659  rprmval  33709  selvply1rhmlem4  33817  evlextv  33836  mplvrpmfgalem  33838  mplvrpmga  33839  mplvrpmmhm  33840  mplvrpmrhm  33841  psrmonmul  33844  esplyfval0  33858  esplyfvaln  33868  locfinreflem  34134  rspectopn  34161  zarcls1  34163  zarclsun  34164  zarclsiin  34165  zarclsint  34166  zarclssn  34167  zarcls  34168  zartopn  34169  zar0ring  34172  zart0  34173  zarmxt1  34174  zarcmplem  34175  rhmpreimacnlem  34178  rhmpreimacn  34179  ordtconnlem1  34218  sigaex  34404  ddemeas  34530  ismbfm  34545  elunirnmbfm  34546  eulerpart  34676  ballotlem8  34831  reprval  34901  bnj110  35150  fncvm  35604  iscvm  35606  snmlval  35678  satfv1  35710  satfdm  35716  satffunlem1lem2  35750  satfv0fvfmla0  35760  satfv1fvfmla1  35770  mpstval  35882  fvray  36488  regsfromregtco  36895  icoreval  37844  fin2solem  38102  fin2so  38103  poimirlem4  38120  cnambfre  38164  istotbnd  38265  isbnd  38276  rngohomval  38460  rngoisoval  38473  idlval  38509  pridlval  38529  maxidlval  38535  lshpset  39599  lflset  39680  pats  39906  llnset  40126  lplnset  40150  lvolset  40193  isline  40360  pmapval  40378  paddval  40419  lhpset  40616  ldilset  40730  ltrnset  40739  dilsetN  40774  trnsetN  40777  diaval  41653  diafn  41655  lpolsetN  42103  lcdvadd  42218  lcdsca  42220  lcdvs  42224  mapdval  42249  mapd1o  42269  unitscyglem5  42813  psrmnd  43158  mhmcopsr  43159  mhmcoaddpsr  43160  rhmcomulpsr  43161  evlselv  43168  mhphf  43176  prjcrvval  43211  isnacs  43282  mzpclval  43303  pell1qrval  43420  pell14qrval  43422  pell1234qrval  43424  elmnc  43710  itgoval  43735  idomodle  43765  idomsubgmo  43767  k0004val  44723  permaxsep  45580  icof  45792  elicores  46106  dvnprodlem1  46517  dvnprodlem2  46518  dvnprodlem3  46519  stoweidlem34  46605  fourierdlem2  46680  fourierdlem3  46681  etransclem12  46817  etransclem33  46838  ovnval2b  47123  volicorescl  47124  ovncvrrp  47135  ovnsubaddlem1  47141  ovncvr2  47182  issmflem  47298  smfaddlem1  47334  smfaddlem2  47335  smflimlem1  47342  fvmptrabdm  47884  iccpval  48018  fppr  48345  grtri  48559  assintopval  48824  rngchomrnghmresALTV  48898  bigoval  49168  elbigofrcl  49169  line  49351  rrxline  49353  sphere  49366  rrxsphere  49367