Theorem rabex 5319

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

Syntax hints:   ∈ wcel 2107  {crab 3419  Vcvv 3463

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-sep 5276

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3420  df-v 3465  df-in 3938  df-ss 3948  df-pw 4582

This theorem is referenced by:  rab2ex  5322  frminex  5644  ssimaex  6974  fvmptrabfv  7028  mptrabex  7227  fnpm  8856  inf3lema  9646  dfac2a  10152  kmlem1  10173  axcc4  10461  axdc3lem2  10473  axdc3lem4  10475  pwfseqlem1  10680  dfuzi  12692  uzval  12862  ixxval  13377  fzval  13531  bitsfval  16442  sadfval  16471  smufval  16496  phicl2  16787  hashgcdeq  16809  prmreclem4  16939  prmreclem5  16940  ismre  17604  fnmre  17605  mrisval  17644  isacs  17665  ismon  17748  isnat  17966  natffn  17968  initofn  18003  termofn  18004  initoval  18009  termoval  18010  coafval  18080  ismgmhm  18678  issubmgm  18684  ismhm  18767  issubm  18785  issubg  19113  isnsg  19142  gimfn  19248  isgim  19249  isga  19278  cntzval  19308  odfval  19518  odngen  19563  gexval  19564  isslw  19594  ablfac1a  20057  ablfac1b  20058  ablfac1c  20059  ablfac1eu  20061  ablfaclem1  20073  ablfaclem2  20074  ablfaclem3  20075  isirred  20387  rnghmfn  20407  rnghmval  20408  isrngim  20413  isrim0OLD  20449  isrim0  20451  issubrng  20515  issubrg  20539  rrgval  20665  issdrg  20757  abvfval  20779  lssset  20899  lmimfn  20993  islmhm  20994  islmim  21029  islbs  21043  ocvval  21639  elocv  21640  isobs  21694  islinds  21783  psrval  21889  psraddcl  21912  psraddclOLD  21913  psrvscacl  21925  psrgrp  21930  psrgrpOLD  21931  psrlmod  21934  subrgpsr  21952  mvrf  21959  mplsubrg  21979  mplmonmul  22008  mplbas2  22014  opsrval  22018  mhpval  22091  mhpmulcl  22101  mhpinvcl  22104  psdcl  22113  psdmplcl  22114  psdadd  22115  psdmul  22118  psrplusgpropd  22185  psropprmul  22187  rhmcomulmpl  22334  scmatval  22458  fncld  22976  cnfval  23187  cnpval  23190  iscnp2  23193  1stcfb  23399  kgenf  23495  xkoopn  23543  dfac14  23572  hmeofn  23711  hmeofval  23712  filunirn  23836  alexsubALTlem2  24002  ucnval  24231  iscfilu  24242  ispsmet  24259  ismet  24278  isxmet  24279  xmetunirn  24292  cncfval  24850  ishtpy  24940  isphtpy  24949  om1bas  25000  cfilfval  25234  caufval  25245  iscmet  25254  dyadmax  25569  vitalilem2  25580  vitalilem3  25581  vitalilem4  25582  itg2monolem1  25721  fncpn  25905  elcpn  25906  mdeg0  26045  mdegaddle  26049  mdegvsca  26051  uc1pval  26115  mon1pval  26117  aannenlem1  26306  aannenlem2  26307  aannenlem3  26308  vmaval  27092  sqff1o  27161  musum  27170  dchrval  27214  dchrbas  27215  leftval  27838  rightval  27839  leftf  27840  rightf  27841  precsexlem4  28170  precsexlem5  28171  tglnfn  28491  tglnunirn  28492  tglngval  28495  israg  28641  iseqlg  28811  ttgitvval  28827  ebtwntg  28927  incistruhgr  29024  usgredgleordALT  29179  vtxdun  29427  vtxdlfgrval  29431  vtxd0nedgb  29434  vtxdushgrfvedglem  29435  vtxdushgrfvedg  29436  vtxdusgr0edgnelALT  29442  1loopgrvd2  29449  usgrvd0nedg  29479  rusgrnumwrdl2  29532  ewlksfval  29547  wwlksn  29785  wspthsn  29796  iswwlksnon  29801  iswspthsnon  29804  wlknwwlksnen  29837  wwlksnexthasheq  29851  rusgrnumwlkg  29925  clwlkclwwlken  29959  clwwlkn  29973  clwwlken  29999  clwlkssizeeq  30032  clwwlknon  30037  clwwlk0on0  30039  konigsberglem5  30203  fusgreg2wsplem  30280  fusgreghash2wsp  30285  2clwwlk  30294  clwwlknonclwlknonen  30310  numclwlk1lem2  30317  numclwwlkovh0  30319  numclwwlkovq  30321  numclwwlkqhash  30322  lnoval  30699  bloval  30728  hmoval  30757  ubthlem1  30817  ubthlem2  30818  ocval  31227  eigvecval  31843  specval  31845  rabfodom  32452  fpwrelmap  32679  nsgmgc  33375  mxidlval  33424  ssmxidl  33437  rprmval  33479  locfinreflem  33798  rspectopn  33825  zarcls1  33827  zarclsun  33828  zarclsiin  33829  zarclsint  33830  zarclssn  33831  zarcls  33832  zartopn  33833  zar0ring  33836  zart0  33837  zarmxt1  33838  zarcmplem  33839  rhmpreimacnlem  33842  rhmpreimacn  33843  ordtconnlem1  33882  sigaex  34070  ddemeas  34196  ismbfm  34211  elunirnmbfm  34212  eulerpart  34343  ballotlem8  34498  reprval  34584  bnj110  34831  fncvm  35221  iscvm  35223  snmlval  35295  satfv1  35327  satfdm  35333  satffunlem1lem2  35367  satfv0fvfmla0  35377  satfv1fvfmla1  35387  mpstval  35499  fvray  36101  icoreval  37313  fin2solem  37572  fin2so  37573  poimirlem4  37590  cnambfre  37634  istotbnd  37735  isbnd  37746  rngohomval  37930  rngoisoval  37943  idlval  37979  pridlval  37999  maxidlval  38005  lshpset  38938  lflset  39019  pats  39245  llnset  39466  lplnset  39490  lvolset  39533  isline  39700  pmapval  39718  paddval  39759  lhpset  39956  ldilset  40070  ltrnset  40079  dilsetN  40114  trnsetN  40117  diaval  40993  diafn  40995  lpolsetN  41443  lcdvadd  41558  lcdsca  41560  lcdvs  41564  mapdval  41589  mapd1o  41609  unitscyglem5  42159  psrmnd  42518  mhmcopsr  42522  mhmcoaddpsr  42523  rhmcomulpsr  42524  evlselv  42560  mhphf  42570  prjcrvval  42605  isnacs  42678  mzpclval  42699  pell1qrval  42820  pell14qrval  42822  pell1234qrval  42824  elmnc  43111  itgoval  43136  idomodle  43166  idomsubgmo  43168  k0004val  44125  icof  45181  elicores  45503  dvnprodlem1  45918  dvnprodlem2  45919  dvnprodlem3  45920  stoweidlem34  46006  fourierdlem2  46081  fourierdlem3  46082  etransclem12  46218  etransclem33  46239  ovnval2b  46524  volicorescl  46525  ovncvrrp  46536  ovnsubaddlem1  46542  ovncvr2  46583  issmflem  46699  smfaddlem1  46735  smfaddlem2  46736  smflimlem1  46743  fvmptrabdm  47263  iccpval  47360  fppr  47671  grtri  47865  assintopval  48079  rngchomrnghmresALTV  48153  bigoval  48428  elbigofrcl  48429  line  48611  rrxline  48613  sphere  48626  rrxsphere  48627