Theorem rabex 5282

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

Syntax hints:   ∈ wcel 2113  {crab 3397  Vcvv 3438

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-in 3906  df-ss 3916  df-pw 4554

This theorem is referenced by:  rab2ex  5285  frminex  5601  ssimaex  6917  fvmptrabfv  6971  mptrabex  7169  fnpm  8769  inf3lema  9531  dfac2a  10038  kmlem1  10059  axcc4  10347  axdc3lem2  10359  axdc3lem4  10361  pwfseqlem1  10567  dfuzi  12581  uzval  12751  ixxval  13267  fzval  13423  bitsfval  16348  sadfval  16377  smufval  16402  phicl2  16693  hashgcdeq  16715  prmreclem4  16845  prmreclem5  16846  ismre  17507  fnmre  17508  mrisval  17551  isacs  17572  ismon  17655  isnat  17872  natffn  17874  initofn  17909  termofn  17910  initoval  17915  termoval  17916  coafval  17986  ismgmhm  18619  issubmgm  18625  ismhm  18708  issubm  18726  issubg  19054  isnsg  19082  gimfn  19188  isgim  19189  isga  19218  cntzval  19248  odfval  19459  odngen  19504  gexval  19505  isslw  19535  ablfac1a  19998  ablfac1b  19999  ablfac1c  20000  ablfac1eu  20002  ablfaclem1  20014  ablfaclem2  20015  ablfaclem3  20016  isirred  20353  rnghmfn  20373  rnghmval  20374  isrngim  20379  isrim0  20416  issubrng  20478  issubrg  20502  rrgval  20628  issdrg  20719  abvfval  20741  lssset  20882  lmimfn  20976  islmhm  20977  islmim  21012  islbs  21026  ocvval  21620  elocv  21621  isobs  21673  islinds  21762  psrval  21869  psraddcl  21892  psraddclOLD  21893  psrvscacl  21905  psrgrp  21910  psrlmod  21913  subrgpsr  21931  mvrf  21938  mplsubrg  21958  mplmonmul  21989  mplbas2  21995  opsrval  21999  mhpval  22080  mhpmulcl  22090  mhpinvcl  22093  psdcl  22102  psdmplcl  22103  psdadd  22104  psdmul  22107  psrplusgpropd  22174  psropprmul  22176  rhmcomulmpl  22324  scmatval  22446  fncld  22964  cnfval  23175  cnpval  23178  iscnp2  23181  1stcfb  23387  kgenf  23483  xkoopn  23531  dfac14  23560  hmeofn  23699  hmeofval  23700  filunirn  23824  alexsubALTlem2  23990  ucnval  24218  iscfilu  24229  ispsmet  24246  ismet  24265  isxmet  24266  xmetunirn  24279  cncfval  24835  ishtpy  24925  isphtpy  24934  om1bas  24985  cfilfval  25218  caufval  25229  iscmet  25238  dyadmax  25553  vitalilem2  25564  vitalilem3  25565  vitalilem4  25566  itg2monolem1  25705  fncpn  25889  elcpn  25890  mdeg0  26029  mdegaddle  26033  mdegvsca  26035  uc1pval  26099  mon1pval  26101  aannenlem1  26290  aannenlem2  26291  aannenlem3  26292  vmaval  27077  sqff1o  27146  musum  27155  dchrval  27199  dchrbas  27200  leftval  27831  rightval  27832  leftf  27837  rightf  27838  precsexlem4  28178  precsexlem5  28179  tglnfn  28568  tglnunirn  28569  tglngval  28572  israg  28718  iseqlg  28888  ttgitvval  28903  ebtwntg  29004  incistruhgr  29101  usgredgleordALT  29256  vtxdun  29504  vtxdlfgrval  29508  vtxd0nedgb  29511  vtxdushgrfvedglem  29512  vtxdushgrfvedg  29513  vtxdusgr0edgnelALT  29519  1loopgrvd2  29526  usgrvd0nedg  29556  rusgrnumwrdl2  29609  ewlksfval  29624  wwlksn  29859  wspthsn  29870  iswwlksnon  29875  iswspthsnon  29878  wlknwwlksnen  29911  wwlksnexthasheq  29925  rusgrnumwlkg  30002  clwlkclwwlken  30036  clwwlkn  30050  clwwlken  30076  clwlkssizeeq  30109  clwwlknon  30114  clwwlk0on0  30116  konigsberglem5  30280  fusgreg2wsplem  30357  fusgreghash2wsp  30362  2clwwlk  30371  clwwlknonclwlknonen  30387  numclwlk1lem2  30394  numclwwlkovh0  30396  numclwwlkovq  30398  numclwwlkqhash  30399  lnoval  30776  bloval  30805  hmoval  30834  ubthlem1  30894  ubthlem2  30895  ocval  31304  eigvecval  31920  specval  31922  rabfodom  32529  fpwrelmap  32761  nsgmgc  33442  mxidlval  33491  ssmxidl  33504  rprmval  33546  evlextv  33656  mplvrpmfgalem  33658  mplvrpmga  33659  mplvrpmmhm  33660  mplvrpmrhm  33661  esplyfval0  33671  locfinreflem  33946  rspectopn  33973  zarcls1  33975  zarclsun  33976  zarclsiin  33977  zarclsint  33978  zarclssn  33979  zarcls  33980  zartopn  33981  zar0ring  33984  zart0  33985  zarmxt1  33986  zarcmplem  33987  rhmpreimacnlem  33990  rhmpreimacn  33991  ordtconnlem1  34030  sigaex  34216  ddemeas  34342  ismbfm  34357  elunirnmbfm  34358  eulerpart  34488  ballotlem8  34643  reprval  34716  bnj110  34963  fncvm  35400  iscvm  35402  snmlval  35474  satfv1  35506  satfdm  35512  satffunlem1lem2  35546  satfv0fvfmla0  35556  satfv1fvfmla1  35566  mpstval  35678  fvray  36284  icoreval  37497  fin2solem  37746  fin2so  37747  poimirlem4  37764  cnambfre  37808  istotbnd  37909  isbnd  37920  rngohomval  38104  rngoisoval  38117  idlval  38153  pridlval  38173  maxidlval  38179  lshpset  39177  lflset  39258  pats  39484  llnset  39704  lplnset  39728  lvolset  39771  isline  39938  pmapval  39956  paddval  39997  lhpset  40194  ldilset  40308  ltrnset  40317  dilsetN  40352  trnsetN  40355  diaval  41231  diafn  41233  lpolsetN  41681  lcdvadd  41796  lcdsca  41798  lcdvs  41802  mapdval  41827  mapd1o  41847  unitscyglem5  42392  psrmnd  42740  mhmcopsr  42744  mhmcoaddpsr  42745  rhmcomulpsr  42746  evlselv  42772  mhphf  42782  prjcrvval  42817  isnacs  42888  mzpclval  42909  pell1qrval  43030  pell14qrval  43032  pell1234qrval  43034  elmnc  43320  itgoval  43345  idomodle  43375  idomsubgmo  43377  k0004val  44333  permaxsep  45190  icof  45405  elicores  45721  dvnprodlem1  46132  dvnprodlem2  46133  dvnprodlem3  46134  stoweidlem34  46220  fourierdlem2  46295  fourierdlem3  46296  etransclem12  46432  etransclem33  46453  ovnval2b  46738  volicorescl  46739  ovncvrrp  46750  ovnsubaddlem1  46756  ovncvr2  46797  issmflem  46913  smfaddlem1  46949  smfaddlem2  46950  smflimlem1  46957  fvmptrabdm  47481  iccpval  47603  fppr  47914  grtri  48128  assintopval  48393  rngchomrnghmresALTV  48467  bigoval  48737  elbigofrcl  48738  line  48920  rrxline  48922  sphere  48935  rrxsphere  48936