Theorem rabex 5300

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

This proof depends on syntax axioms:   ∈ wcel 2145  {crab 3413  Vcvv 3451

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-in 3906  df-ss 3916  df-pw 4559

This theorem is used by:  rab2ex  5303  frminex  5630  ssimaex  6968  fvmptrabfv  7024  mptrabex  7229  fnpm  8847  inf3lema  9618  dfac2a  10201  kmlem1  10222  axcc4  10510  axdc3lem2  10522  axdc3lem4  10524  pwfseqlem1  10736  dfuzi  12783  uzval  12960  ixxval  13477  fzval  13634  bitsfval  16586  sadfval  16615  smufval  16640  phicl2  16938  hashgcdeq  16960  prmreclem4  17090  prmreclem5  17091  ismre  17753  fnmre  17754  mrisval  17797  isacs  17818  ismon  17901  isnat  18118  natffn  18120  initofn  18155  termofn  18156  initoval  18161  termoval  18162  coafval  18232  ismgmhm  18878  issubmgm  18884  ismhm  18973  issubm  18991  issubg  19329  isnsg  19358  gimfn  19468  isgim  19469  isga  19498  cntzval  19528  odfval  19739  odngen  19784  gexval  19785  isslw  19815  ablfac1a  20278  ablfac1b  20279  ablfac1c  20280  ablfac1eu  20282  ablfaclem1  20294  ablfaclem2  20295  ablfaclem3  20296  isirred  20642  rnghmfn  20662  rnghmval  20663  isrngim  20668  rhmval0  20698  isrim0  20706  rimfn  20730  issubrng  20792  issubrg  20816  rrgval  20942  issdrg  21038  abvfval  21060  lssset  21201  lmimfn  21294  islmhm  21295  islmim  21330  islbs  21344  ocvval  21966  elocv  21967  isobs  22019  islinds  22108  psrval  22216  psraddcl  22240  psrvscacl  22252  psrgrp  22257  psrlmod  22260  subrgpsr  22278  mvrf  22285  mplsubrg  22305  mplmonmul  22338  mplbas2  22344  opsrval  22348  rhmcomulmpl  22426  mhpval  22453  mhpmulcl  22463  mhpinvcl  22466  psdcl  22475  psdmplcl  22476  psdadd  22477  psdmul  22480  psrplusgpropd  22546  psropprmul  22548  scmatval  22812  fncld  23333  cnfval  23544  cnpval  23547  iscnp2  23550  1stcfb  23756  kgenf  23853  xkoopn  23901  dfac14  23930  hmeofn  24069  hmeofval  24070  filunirn  24194  alexsubALTlem2  24360  ucnval  24588  iscfilu  24599  ispsmet  24616  ismet  24635  isxmet  24636  xmetunirn  24649  cncfval  25202  ishtpy  25286  isphtpy  25295  om1bas  25345  cfilfval  25578  caufval  25589  iscmet  25598  dyadmax  25912  vitalilem2  25923  vitalilem3  25924  vitalilem4  25925  itg2monolem1  26064  fncpn  26246  elcpn  26247  mdeg0  26381  mdegaddle  26385  mdegvsca  26387  uc1pval  26451  mon1pval  26453  aannenlem1  26648  aannenlem2  26649  aannenlem3  26650  vmaval  27433  sqff1o  27502  musum  27511  dchrval  27554  dchrbas  27555  leftval  28228  rightval  28229  leftf  28234  rightf  28235  precsexlem4  28589  precsexlem5  28590  tglnfn  29003  tglnunirn  29004  tglngval  29007  israg  29165  tgplnfn  29246  isplng  29249  iseqlg  29405  ttgitvval  29452  ebtwntg  29553  incistruhgr  29650  usgredgleordALT  29808  vtxdun  30055  vtxdlfgrval  30059  vtxd0nedgb  30062  vtxdushgrfvedglem  30063  vtxdushgrfvedg  30064  vtxdusgr0edgnelALT  30070  1loopgrvd2  30077  usgrvd0nedg  30107  rusgrnumwrdl2  30160  ewlksfval  30175  wwlksn  30419  wspthsn  30430  iswwlksnon  30435  iswspthsnon  30438  wlknwwlksnen  30471  wwlksnexthasheq  30485  rusgrnumwlkg  30562  clwlkclwwlken  30596  clwwlkn  30610  clwwlken  30636  clwlkssizeeq  30669  clwwlknon  30674  clwwlk0on0  30676  konigsberglem5  30850  fusgreg2wsplem  30927  fusgreghash2wsp  30932  2clwwlk  30941  clwwlknonclwlknonen  30957  numclwlk1lem2  30964  numclwwlkovh0  30966  numclwwlkovq  30968  numclwwlkqhash  30969  lnoval  31347  bloval  31376  hmoval  31405  ubthlem1  31465  ubthlem2  31466  ocval  31875  eigvecval  32491  specval  32493  rabfodom  33094  fpwrelmap  33318  nsgmgc  33956  mxidlval  33979  ssmxidl  33992  rprmval  34041  selvply1rhmlem4  34148  evlextv  34167  mplvrpmfgalem  34169  mplvrpmga  34170  mplvrpmmhm  34171  mplvrpmrhm  34172  psrmonmul  34175  esplyfval0  34189  esplyfvaln  34199  locfinreflem  34465  rspectopn  34492  zarcls1  34494  zarclsun  34495  zarclsiin  34496  zarclsint  34497  zarclssn  34498  zarcls  34499  zartopn  34500  zar0ring  34503  zart0  34504  zarmxt1  34505  zarcmplem  34506  rhmpreimacnlem  34509  rhmpreimacn  34510  ordtconnlem1  34549  sigaex  34735  ddemeas  34862  ismbfm  34877  elunirnmbfm  34878  eulerpart  35007  ballotlem8  35162  reprval  35232  bnj110  35481  fncvm  36001  iscvm  36003  snmlval  36075  satfv1  36107  satfdm  36113  satffunlem1lem2  36147  satfv0fvfmla0  36157  satfv1fvfmla1  36167  mpstval  36279  fvray  36886  regsfromregtco  37306  icoreval  38256  fin2solem  38509  fin2so  38510  poimirlem4  38522  cnambfre  38566  istotbnd  38683  isbnd  38694  rngohomval  38878  rngoisoval  38891  idlval  38927  pridlval  38947  maxidlval  38953  lshpset  40015  lflset  40096  pats  40322  llnset  40542  lplnset  40566  lvolset  40609  isline  40776  pmapval  40794  paddval  40835  lhpset  41032  ldilset  41146  ltrnset  41155  dilsetN  41190  trnsetN  41193  diaval  42069  diafn  42071  lpolsetN  42519  lcdvadd  42634  lcdsca  42636  lcdvs  42640  mapdval  42665  mapd1o  42685  unitscyglem5  43229  psrmnd  43587  mhmcopsr  43588  mhmcoaddpsr  43589  rhmcomulpsr  43590  evlselv  43597  mhphf  43605  prjcrvval  43648  isnacs  43694  mzpclval  43715  pell1qrval  43832  pell14qrval  43834  pell1234qrval  43836  elmnc  44122  itgoval  44147  idomodle  44177  idomsubgmo  44179  k0004val  45135  permaxsep  45975  icof  46201  elicores  46514  dvnprodlem1  46925  dvnprodlem2  46926  dvnprodlem3  46927  stoweidlem34  47013  fourierdlem2  47088  fourierdlem3  47089  etransclem12  47225  etransclem33  47246  ovnval2b  47531  volicorescl  47532  ovncvrrp  47543  ovnsubaddlem1  47549  ovncvr2  47590  issmflem  47706  smfaddlem1  47742  smfaddlem2  47743  smflimlem1  47750  fvmptrabdm  48332  iccpval  48466  fppr  48793  grtri  49007  assintopval  49271  rngchomrnghmresALTV  49345  bigoval  49630  elbigofrcl  49631  line  49813  rrxline  49815  sphere  49828  rrxsphere  49829