Theorem rabex 5251

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

Syntax hints:   ∈ wcel 2108  {crab 3067  Vcvv 3422

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  rab2ex  5254  frminex  5560  ssimaex  6835  fvmptrabfv  6888  mptrabex  7083  fnpm  8581  inf3lema  9312  dfac2a  9816  kmlem1  9837  axcc4  10126  axdc3lem2  10138  axdc3lem4  10140  pwfseqlem1  10345  dfuzi  12341  uzval  12513  ixxval  13016  fzval  13170  bitsfval  16058  sadfval  16087  smufval  16112  phicl2  16397  hashgcdeq  16418  prmreclem4  16548  prmreclem5  16549  ismre  17216  fnmre  17217  mrisval  17256  isacs  17277  ismon  17362  isnat  17579  natffn  17581  initofn  17618  termofn  17619  initoval  17624  termoval  17625  coafval  17695  ismhm  18347  issubm  18357  issubg  18670  isnsg  18698  gimfn  18792  isgim  18793  isga  18812  cntzval  18842  odfval  19055  odngen  19097  gexval  19098  isslw  19128  ablfac1a  19587  ablfac1b  19588  ablfac1c  19589  ablfac1eu  19591  ablfaclem1  19603  ablfaclem2  19604  ablfaclem3  19605  isirred  19856  isrim0  19882  issubrg  19939  issdrg  19978  abvfval  19993  lssset  20110  lmimfn  20203  islmhm  20204  islmim  20239  islbs  20253  rrgval  20471  ocvval  20784  elocv  20785  isobs  20837  islinds  20926  psrval  21028  psraddcl  21062  psrvscacl  21072  psrgrp  21077  psrlmod  21080  subrgpsr  21098  mvrf  21103  mplsubrg  21121  mplmonmul  21147  mplbas2  21153  opsrval  21157  mhpval  21240  mhpmulcl  21249  mhpinvcl  21252  psrplusgpropd  21317  psropprmul  21319  scmatval  21561  fncld  22081  cnfval  22292  cnpval  22295  iscnp2  22298  1stcfb  22504  kgenf  22600  xkoopn  22648  dfac14  22677  hmeofn  22816  hmeofval  22817  filunirn  22941  alexsubALTlem2  23107  ucnval  23337  iscfilu  23348  ispsmet  23365  ismet  23384  isxmet  23385  xmetunirn  23398  cncfval  23957  ishtpy  24041  isphtpy  24050  om1bas  24100  cfilfval  24333  caufval  24344  iscmet  24353  dyadmax  24667  vitalilem2  24678  vitalilem3  24679  vitalilem4  24680  itg2monolem1  24820  fncpn  25002  elcpn  25003  mdeg0  25140  mdegaddle  25144  mdegvsca  25146  uc1pval  25209  mon1pval  25211  aannenlem1  25393  aannenlem2  25394  aannenlem3  25395  vmaval  26167  sqff1o  26236  musum  26245  dchrval  26287  dchrbas  26288  tglnfn  26812  tglnunirn  26813  tglngval  26816  israg  26962  iseqlg  27132  ttgitvval  27152  ebtwntg  27253  incistruhgr  27352  usgredgleordALT  27504  vtxdun  27751  vtxdlfgrval  27755  vtxd0nedgb  27758  vtxdushgrfvedglem  27759  vtxdushgrfvedg  27760  vtxdusgr0edgnelALT  27766  1loopgrvd2  27773  usgrvd0nedg  27803  rusgrnumwrdl2  27856  ewlksfval  27871  wwlksn  28103  wspthsn  28114  iswwlksnon  28119  iswspthsnon  28122  wlknwwlksnen  28155  wwlksnexthasheq  28169  rusgrnumwlkg  28243  clwlkclwwlken  28277  clwwlkn  28291  clwwlken  28317  clwlkssizeeq  28350  clwwlknon  28355  clwwlk0on0  28357  konigsberglem5  28521  fusgreg2wsplem  28598  fusgreghash2wsp  28603  2clwwlk  28612  clwwlknonclwlknonen  28628  numclwlk1lem2  28635  numclwwlkovh0  28637  numclwwlkovq  28639  numclwwlkqhash  28640  lnoval  29015  bloval  29044  hmoval  29073  ubthlem1  29133  ubthlem2  29134  ocval  29543  eigvecval  30159  specval  30161  rabfodom  30752  fpwrelmap  30970  nsgmgc  31499  mxidlval  31535  ssmxidl  31544  rprmval  31566  locfinreflem  31692  rspectopn  31719  zarcls1  31721  zarclsun  31722  zarclsiin  31723  zarclsint  31724  zarclssn  31725  zarcls  31726  zartopn  31727  zar0ring  31730  zart0  31731  zarmxt1  31732  zarcmplem  31733  rhmpreimacnlem  31736  rhmpreimacn  31737  ordtconnlem1  31776  sigaex  31978  ddemeas  32104  ismbfm  32119  elunirnmbfm  32120  eulerpart  32249  ballotlem8  32403  reprval  32490  bnj110  32738  fncvm  33119  iscvm  33121  snmlval  33193  satfv1  33225  satfdm  33231  satffunlem1lem2  33265  satfv0fvfmla0  33275  satfv1fvfmla1  33285  mpstval  33397  leftval  33974  rightval  33975  leftf  33976  rightf  33977  fvray  34370  icoreval  35451  fin2solem  35690  fin2so  35691  poimirlem4  35708  cnambfre  35752  istotbnd  35854  isbnd  35865  rngohomval  36049  rngoisoval  36062  idlval  36098  pridlval  36118  maxidlval  36124  lshpset  36919  lflset  37000  pats  37226  llnset  37446  lplnset  37470  lvolset  37513  isline  37680  pmapval  37698  paddval  37739  lhpset  37936  ldilset  38050  ltrnset  38059  dilsetN  38094  trnsetN  38097  diaval  38973  diafn  38975  lpolsetN  39423  lcdvadd  39538  lcdsca  39540  lcdvs  39544  mapdval  39569  mapd1o  39589  selvval2lem4  40154  mhphf  40208  isnacs  40442  mzpclval  40463  pell1qrval  40584  pell14qrval  40586  pell1234qrval  40588  elmnc  40877  itgoval  40902  idomodle  40937  idomsubgmo  40939  k0004val  41649  icof  42648  elicores  42961  dvnprodlem1  43377  dvnprodlem2  43378  dvnprodlem3  43379  stoweidlem34  43465  fourierdlem2  43540  fourierdlem3  43541  etransclem12  43677  etransclem33  43698  ovnval2b  43980  volicorescl  43981  ovncvrrp  43992  ovnsubaddlem1  43998  ovncvr2  44039  issmflem  44150  smfaddlem1  44185  smfaddlem2  44186  smflimlem1  44193  fvmptrabdm  44672  iccpval  44755  fppr  45066  ismgmhm  45225  issubmgm  45231  assintopval  45287  rnghmfn  45336  rnghmval  45337  isrngisom  45342  rngchomrnghmresALTV  45442  bigoval  45783  elbigofrcl  45784  line  45966  rrxline  45968  sphere  45981  rrxsphere  45982