Theorem rabex 5277

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

Syntax hints:   ∈ wcel 2114  {crab 3390  Vcvv 3430

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 5232

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 3391  df-v 3432  df-in 3897  df-ss 3907  df-pw 4544

This theorem is referenced by:  rab2ex  5280  frminex  5604  ssimaex  6920  fvmptrabfv  6975  mptrabex  7174  fnpm  8775  inf3lema  9539  dfac2a  10046  kmlem1  10067  axcc4  10355  axdc3lem2  10367  axdc3lem4  10369  pwfseqlem1  10575  dfuzi  12614  uzval  12784  ixxval  13300  fzval  13457  bitsfval  16386  sadfval  16415  smufval  16440  phicl2  16732  hashgcdeq  16754  prmreclem4  16884  prmreclem5  16885  ismre  17546  fnmre  17547  mrisval  17590  isacs  17611  ismon  17694  isnat  17911  natffn  17913  initofn  17948  termofn  17949  initoval  17954  termoval  17955  coafval  18025  ismgmhm  18658  issubmgm  18664  ismhm  18747  issubm  18765  issubg  19096  isnsg  19124  gimfn  19230  isgim  19231  isga  19260  cntzval  19290  odfval  19501  odngen  19546  gexval  19547  isslw  19577  ablfac1a  20040  ablfac1b  20041  ablfac1c  20042  ablfac1eu  20044  ablfaclem1  20056  ablfaclem2  20057  ablfaclem3  20058  isirred  20393  rnghmfn  20413  rnghmval  20414  isrngim  20419  isrim0  20456  issubrng  20518  issubrg  20542  rrgval  20668  issdrg  20759  abvfval  20781  lssset  20922  lmimfn  21016  islmhm  21017  islmim  21052  islbs  21066  ocvval  21660  elocv  21661  isobs  21713  islinds  21802  psrval  21908  psraddcl  21931  psrvscacl  21943  psrgrp  21948  psrlmod  21951  subrgpsr  21969  mvrf  21976  mplsubrg  21996  mplmonmul  22027  mplbas2  22033  opsrval  22037  mhpval  22118  mhpmulcl  22128  mhpinvcl  22131  psdcl  22140  psdmplcl  22141  psdadd  22142  psdmul  22145  psrplusgpropd  22212  psropprmul  22214  rhmcomulmpl  22360  scmatval  22482  fncld  23000  cnfval  23211  cnpval  23214  iscnp2  23217  1stcfb  23423  kgenf  23519  xkoopn  23567  dfac14  23596  hmeofn  23735  hmeofval  23736  filunirn  23860  alexsubALTlem2  24026  ucnval  24254  iscfilu  24265  ispsmet  24282  ismet  24301  isxmet  24302  xmetunirn  24315  cncfval  24868  ishtpy  24952  isphtpy  24961  om1bas  25011  cfilfval  25244  caufval  25255  iscmet  25264  dyadmax  25578  vitalilem2  25589  vitalilem3  25590  vitalilem4  25591  itg2monolem1  25730  fncpn  25913  elcpn  25914  mdeg0  26048  mdegaddle  26052  mdegvsca  26054  uc1pval  26118  mon1pval  26120  aannenlem1  26308  aannenlem2  26309  aannenlem3  26310  vmaval  27093  sqff1o  27162  musum  27171  dchrval  27214  dchrbas  27215  leftval  27858  rightval  27859  leftf  27864  rightf  27865  precsexlem4  28219  precsexlem5  28220  tglnfn  28632  tglnunirn  28633  tglngval  28636  israg  28782  iseqlg  28952  ttgitvval  28967  ebtwntg  29068  incistruhgr  29165  usgredgleordALT  29320  vtxdun  29568  vtxdlfgrval  29572  vtxd0nedgb  29575  vtxdushgrfvedglem  29576  vtxdushgrfvedg  29577  vtxdusgr0edgnelALT  29583  1loopgrvd2  29590  usgrvd0nedg  29620  rusgrnumwrdl2  29673  ewlksfval  29688  wwlksn  29923  wspthsn  29934  iswwlksnon  29939  iswspthsnon  29942  wlknwwlksnen  29975  wwlksnexthasheq  29989  rusgrnumwlkg  30066  clwlkclwwlken  30100  clwwlkn  30114  clwwlken  30140  clwlkssizeeq  30173  clwwlknon  30178  clwwlk0on0  30180  konigsberglem5  30344  fusgreg2wsplem  30421  fusgreghash2wsp  30426  2clwwlk  30435  clwwlknonclwlknonen  30451  numclwlk1lem2  30458  numclwwlkovh0  30460  numclwwlkovq  30462  numclwwlkqhash  30463  lnoval  30841  bloval  30870  hmoval  30899  ubthlem1  30959  ubthlem2  30960  ocval  31369  eigvecval  31985  specval  31987  rabfodom  32593  fpwrelmap  32824  nsgmgc  33490  mxidlval  33539  ssmxidl  33552  rprmval  33594  evlextv  33704  mplvrpmfgalem  33706  mplvrpmga  33707  mplvrpmmhm  33708  mplvrpmrhm  33709  psrmonmul  33712  esplyfval0  33726  esplyfvaln  33736  locfinreflem  34003  rspectopn  34030  zarcls1  34032  zarclsun  34033  zarclsiin  34034  zarclsint  34035  zarclssn  34036  zarcls  34037  zartopn  34038  zar0ring  34041  zart0  34042  zarmxt1  34043  zarcmplem  34044  rhmpreimacnlem  34047  rhmpreimacn  34048  ordtconnlem1  34087  sigaex  34273  ddemeas  34399  ismbfm  34414  elunirnmbfm  34415  eulerpart  34545  ballotlem8  34700  reprval  34773  bnj110  35019  fncvm  35458  iscvm  35460  snmlval  35532  satfv1  35564  satfdm  35570  satffunlem1lem2  35604  satfv0fvfmla0  35614  satfv1fvfmla1  35624  mpstval  35736  fvray  36342  regsfromregtco  36739  icoreval  37686  fin2solem  37944  fin2so  37945  poimirlem4  37962  cnambfre  38006  istotbnd  38107  isbnd  38118  rngohomval  38302  rngoisoval  38315  idlval  38351  pridlval  38371  maxidlval  38377  lshpset  39441  lflset  39522  pats  39748  llnset  39968  lplnset  39992  lvolset  40035  isline  40202  pmapval  40220  paddval  40261  lhpset  40458  ldilset  40572  ltrnset  40581  dilsetN  40616  trnsetN  40619  diaval  41495  diafn  41497  lpolsetN  41945  lcdvadd  42060  lcdsca  42062  lcdvs  42066  mapdval  42091  mapd1o  42111  unitscyglem5  42655  psrmnd  43005  mhmcopsr  43009  mhmcoaddpsr  43010  rhmcomulpsr  43011  evlselv  43037  mhphf  43047  prjcrvval  43082  isnacs  43153  mzpclval  43174  pell1qrval  43295  pell14qrval  43297  pell1234qrval  43299  elmnc  43585  itgoval  43610  idomodle  43640  idomsubgmo  43642  k0004val  44598  permaxsep  45455  icof  45669  elicores  45984  dvnprodlem1  46395  dvnprodlem2  46396  dvnprodlem3  46397  stoweidlem34  46483  fourierdlem2  46558  fourierdlem3  46559  etransclem12  46695  etransclem33  46716  ovnval2b  47001  volicorescl  47002  ovncvrrp  47013  ovnsubaddlem1  47019  ovncvr2  47060  issmflem  47176  smfaddlem1  47212  smfaddlem2  47213  smflimlem1  47220  fvmptrabdm  47756  iccpval  47890  fppr  48217  grtri  48431  assintopval  48696  rngchomrnghmresALTV  48770  bigoval  49040  elbigofrcl  49041  line  49223  rrxline  49225  sphere  49238  rrxsphere  49239