Theorem rabex 5338

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

Syntax hints:   ∈ wcel 2098  {crab 3430  Vcvv 3473

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699  ax-sep 5303

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3431  df-v 3475  df-in 3956  df-ss 3966

This theorem is referenced by:  rab2ex  5341  frminex  5662  ssimaex  6988  fvmptrabfv  7042  mptrabex  7243  fnpm  8859  inf3lema  9655  dfac2a  10160  kmlem1  10181  axcc4  10470  axdc3lem2  10482  axdc3lem4  10484  pwfseqlem1  10689  dfuzi  12691  uzval  12862  ixxval  13372  fzval  13526  bitsfval  16405  sadfval  16434  smufval  16459  phicl2  16744  hashgcdeq  16765  prmreclem4  16895  prmreclem5  16896  ismre  17577  fnmre  17578  mrisval  17617  isacs  17638  ismon  17723  isnat  17944  natffn  17946  initofn  17983  termofn  17984  initoval  17989  termoval  17990  coafval  18060  ismgmhm  18663  issubmgm  18669  ismhm  18749  issubm  18762  issubg  19088  isnsg  19117  gimfn  19222  isgim  19223  isga  19249  cntzval  19279  odfval  19494  odngen  19539  gexval  19540  isslw  19570  ablfac1a  20033  ablfac1b  20034  ablfac1c  20035  ablfac1eu  20037  ablfaclem1  20049  ablfaclem2  20050  ablfaclem3  20051  isirred  20365  rnghmfn  20385  rnghmval  20386  isrngim  20391  isrim0OLD  20427  isrim0  20429  issubrng  20491  issubrg  20517  issdrg  20683  abvfval  20705  lssset  20824  lmimfn  20918  islmhm  20919  islmim  20954  islbs  20968  rrgval  21241  ocvval  21606  elocv  21607  isobs  21661  islinds  21750  psrval  21855  psraddcl  21890  psraddclOLD  21891  psrvscacl  21901  psrgrp  21906  psrgrpOLD  21907  psrlmod  21910  subrgpsr  21928  mvrf  21934  mplsubrg  21954  mplmonmul  21981  mplbas2  21987  opsrval  21991  mhpval  22071  mhpmulcl  22080  mhpinvcl  22083  psdcl  22092  psdmplcl  22093  psdadd  22094  psdmul  22097  psrplusgpropd  22161  psropprmul  22163  scmatval  22426  fncld  22946  cnfval  23157  cnpval  23160  iscnp2  23163  1stcfb  23369  kgenf  23465  xkoopn  23513  dfac14  23542  hmeofn  23681  hmeofval  23682  filunirn  23806  alexsubALTlem2  23972  ucnval  24202  iscfilu  24213  ispsmet  24230  ismet  24249  isxmet  24250  xmetunirn  24263  cncfval  24828  ishtpy  24918  isphtpy  24927  om1bas  24978  cfilfval  25212  caufval  25223  iscmet  25232  dyadmax  25547  vitalilem2  25558  vitalilem3  25559  vitalilem4  25560  itg2monolem1  25700  fncpn  25883  elcpn  25884  mdeg0  26026  mdegaddle  26030  mdegvsca  26032  uc1pval  26095  mon1pval  26097  aannenlem1  26283  aannenlem2  26284  aannenlem3  26285  vmaval  27065  sqff1o  27134  musum  27143  dchrval  27187  dchrbas  27188  leftval  27810  rightval  27811  leftf  27812  rightf  27813  precsexlem4  28128  precsexlem5  28129  tglnfn  28371  tglnunirn  28372  tglngval  28375  israg  28521  iseqlg  28691  ttgitvval  28712  ebtwntg  28813  incistruhgr  28912  usgredgleordALT  29067  vtxdun  29315  vtxdlfgrval  29319  vtxd0nedgb  29322  vtxdushgrfvedglem  29323  vtxdushgrfvedg  29324  vtxdusgr0edgnelALT  29330  1loopgrvd2  29337  usgrvd0nedg  29367  rusgrnumwrdl2  29420  ewlksfval  29435  wwlksn  29668  wspthsn  29679  iswwlksnon  29684  iswspthsnon  29687  wlknwwlksnen  29720  wwlksnexthasheq  29734  rusgrnumwlkg  29808  clwlkclwwlken  29842  clwwlkn  29856  clwwlken  29882  clwlkssizeeq  29915  clwwlknon  29920  clwwlk0on0  29922  konigsberglem5  30086  fusgreg2wsplem  30163  fusgreghash2wsp  30168  2clwwlk  30177  clwwlknonclwlknonen  30193  numclwlk1lem2  30200  numclwwlkovh0  30202  numclwwlkovq  30204  numclwwlkqhash  30205  lnoval  30582  bloval  30611  hmoval  30640  ubthlem1  30700  ubthlem2  30701  ocval  31110  eigvecval  31726  specval  31728  rabfodom  32322  fpwrelmap  32536  nsgmgc  33147  mxidlval  33199  ssmxidl  33212  rprmval  33258  locfinreflem  33474  rspectopn  33501  zarcls1  33503  zarclsun  33504  zarclsiin  33505  zarclsint  33506  zarclssn  33507  zarcls  33508  zartopn  33509  zar0ring  33512  zart0  33513  zarmxt1  33514  zarcmplem  33515  rhmpreimacnlem  33518  rhmpreimacn  33519  ordtconnlem1  33558  sigaex  33762  ddemeas  33888  ismbfm  33903  elunirnmbfm  33904  eulerpart  34035  ballotlem8  34189  reprval  34275  bnj110  34522  fncvm  34900  iscvm  34902  snmlval  34974  satfv1  35006  satfdm  35012  satffunlem1lem2  35046  satfv0fvfmla0  35056  satfv1fvfmla1  35066  mpstval  35178  fvray  35770  icoreval  36865  fin2solem  37112  fin2so  37113  poimirlem4  37130  cnambfre  37174  istotbnd  37275  isbnd  37286  rngohomval  37470  rngoisoval  37483  idlval  37519  pridlval  37539  maxidlval  37545  lshpset  38482  lflset  38563  pats  38789  llnset  39010  lplnset  39034  lvolset  39077  isline  39244  pmapval  39262  paddval  39303  lhpset  39500  ldilset  39614  ltrnset  39623  dilsetN  39658  trnsetN  39661  diaval  40537  diafn  40539  lpolsetN  40987  lcdvadd  41102  lcdsca  41104  lcdvs  41108  mapdval  41133  mapd1o  41153  psrmnd  41806  mhmcompl  41812  mhmcoaddmpl  41815  rhmcomulmpl  41816  evlselv  41851  mhphf  41861  prjcrvval  42087  isnacs  42155  mzpclval  42176  pell1qrval  42297  pell14qrval  42299  pell1234qrval  42301  elmnc  42591  itgoval  42616  idomodle  42650  idomsubgmo  42652  k0004val  43611  icof  44622  elicores  44947  dvnprodlem1  45363  dvnprodlem2  45364  dvnprodlem3  45365  stoweidlem34  45451  fourierdlem2  45526  fourierdlem3  45527  etransclem12  45663  etransclem33  45684  ovnval2b  45969  volicorescl  45970  ovncvrrp  45981  ovnsubaddlem1  45987  ovncvr2  46028  issmflem  46144  smfaddlem1  46180  smfaddlem2  46181  smflimlem1  46188  fvmptrabdm  46702  iccpval  46784  fppr  47095  assintopval  47345  rngchomrnghmresALTV  47419  bigoval  47700  elbigofrcl  47701  line  47883  rrxline  47885  sphere  47898  rrxsphere  47899