Theorem rabex 5284

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

Syntax hints:   ∈ wcel 2113  {crab 3399  Vcvv 3440

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 2708  ax-sep 5241

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-in 3908  df-ss 3918  df-pw 4556

This theorem is referenced by:  rab2ex  5287  frminex  5603  ssimaex  6919  fvmptrabfv  6973  mptrabex  7171  fnpm  8771  inf3lema  9533  dfac2a  10040  kmlem1  10061  axcc4  10349  axdc3lem2  10361  axdc3lem4  10363  pwfseqlem1  10569  dfuzi  12583  uzval  12753  ixxval  13269  fzval  13425  bitsfval  16350  sadfval  16379  smufval  16404  phicl2  16695  hashgcdeq  16717  prmreclem4  16847  prmreclem5  16848  ismre  17509  fnmre  17510  mrisval  17553  isacs  17574  ismon  17657  isnat  17874  natffn  17876  initofn  17911  termofn  17912  initoval  17917  termoval  17918  coafval  17988  ismgmhm  18621  issubmgm  18627  ismhm  18710  issubm  18728  issubg  19056  isnsg  19084  gimfn  19190  isgim  19191  isga  19220  cntzval  19250  odfval  19461  odngen  19506  gexval  19507  isslw  19537  ablfac1a  20000  ablfac1b  20001  ablfac1c  20002  ablfac1eu  20004  ablfaclem1  20016  ablfaclem2  20017  ablfaclem3  20018  isirred  20355  rnghmfn  20375  rnghmval  20376  isrngim  20381  isrim0  20418  issubrng  20480  issubrg  20504  rrgval  20630  issdrg  20721  abvfval  20743  lssset  20884  lmimfn  20978  islmhm  20979  islmim  21014  islbs  21028  ocvval  21622  elocv  21623  isobs  21675  islinds  21764  psrval  21871  psraddcl  21894  psraddclOLD  21895  psrvscacl  21907  psrgrp  21912  psrlmod  21915  subrgpsr  21933  mvrf  21940  mplsubrg  21960  mplmonmul  21991  mplbas2  21997  opsrval  22001  mhpval  22082  mhpmulcl  22092  mhpinvcl  22095  psdcl  22104  psdmplcl  22105  psdadd  22106  psdmul  22109  psrplusgpropd  22176  psropprmul  22178  rhmcomulmpl  22326  scmatval  22448  fncld  22966  cnfval  23177  cnpval  23180  iscnp2  23183  1stcfb  23389  kgenf  23485  xkoopn  23533  dfac14  23562  hmeofn  23701  hmeofval  23702  filunirn  23826  alexsubALTlem2  23992  ucnval  24220  iscfilu  24231  ispsmet  24248  ismet  24267  isxmet  24268  xmetunirn  24281  cncfval  24837  ishtpy  24927  isphtpy  24936  om1bas  24987  cfilfval  25220  caufval  25231  iscmet  25240  dyadmax  25555  vitalilem2  25566  vitalilem3  25567  vitalilem4  25568  itg2monolem1  25707  fncpn  25891  elcpn  25892  mdeg0  26031  mdegaddle  26035  mdegvsca  26037  uc1pval  26101  mon1pval  26103  aannenlem1  26292  aannenlem2  26293  aannenlem3  26294  vmaval  27079  sqff1o  27148  musum  27157  dchrval  27201  dchrbas  27202  leftval  27845  rightval  27846  leftf  27851  rightf  27852  precsexlem4  28206  precsexlem5  28207  tglnfn  28619  tglnunirn  28620  tglngval  28623  israg  28769  iseqlg  28939  ttgitvval  28954  ebtwntg  29055  incistruhgr  29152  usgredgleordALT  29307  vtxdun  29555  vtxdlfgrval  29559  vtxd0nedgb  29562  vtxdushgrfvedglem  29563  vtxdushgrfvedg  29564  vtxdusgr0edgnelALT  29570  1loopgrvd2  29577  usgrvd0nedg  29607  rusgrnumwrdl2  29660  ewlksfval  29675  wwlksn  29910  wspthsn  29921  iswwlksnon  29926  iswspthsnon  29929  wlknwwlksnen  29962  wwlksnexthasheq  29976  rusgrnumwlkg  30053  clwlkclwwlken  30087  clwwlkn  30101  clwwlken  30127  clwlkssizeeq  30160  clwwlknon  30165  clwwlk0on0  30167  konigsberglem5  30331  fusgreg2wsplem  30408  fusgreghash2wsp  30413  2clwwlk  30422  clwwlknonclwlknonen  30438  numclwlk1lem2  30445  numclwwlkovh0  30447  numclwwlkovq  30449  numclwwlkqhash  30450  lnoval  30827  bloval  30856  hmoval  30885  ubthlem1  30945  ubthlem2  30946  ocval  31355  eigvecval  31971  specval  31973  rabfodom  32580  fpwrelmap  32812  nsgmgc  33493  mxidlval  33542  ssmxidl  33555  rprmval  33597  evlextv  33707  mplvrpmfgalem  33709  mplvrpmga  33710  mplvrpmmhm  33711  mplvrpmrhm  33712  esplyfval0  33722  locfinreflem  33997  rspectopn  34024  zarcls1  34026  zarclsun  34027  zarclsiin  34028  zarclsint  34029  zarclssn  34030  zarcls  34031  zartopn  34032  zar0ring  34035  zart0  34036  zarmxt1  34037  zarcmplem  34038  rhmpreimacnlem  34041  rhmpreimacn  34042  ordtconnlem1  34081  sigaex  34267  ddemeas  34393  ismbfm  34408  elunirnmbfm  34409  eulerpart  34539  ballotlem8  34694  reprval  34767  bnj110  35014  fncvm  35451  iscvm  35453  snmlval  35525  satfv1  35557  satfdm  35563  satffunlem1lem2  35597  satfv0fvfmla0  35607  satfv1fvfmla1  35617  mpstval  35729  fvray  36335  regsfromregtr  36668  icoreval  37558  fin2solem  37807  fin2so  37808  poimirlem4  37825  cnambfre  37869  istotbnd  37970  isbnd  37981  rngohomval  38165  rngoisoval  38178  idlval  38214  pridlval  38234  maxidlval  38240  lshpset  39238  lflset  39319  pats  39545  llnset  39765  lplnset  39789  lvolset  39832  isline  39999  pmapval  40017  paddval  40058  lhpset  40255  ldilset  40369  ltrnset  40378  dilsetN  40413  trnsetN  40416  diaval  41292  diafn  41294  lpolsetN  41742  lcdvadd  41857  lcdsca  41859  lcdvs  41863  mapdval  41888  mapd1o  41908  unitscyglem5  42453  psrmnd  42798  mhmcopsr  42802  mhmcoaddpsr  42803  rhmcomulpsr  42804  evlselv  42830  mhphf  42840  prjcrvval  42875  isnacs  42946  mzpclval  42967  pell1qrval  43088  pell14qrval  43090  pell1234qrval  43092  elmnc  43378  itgoval  43403  idomodle  43433  idomsubgmo  43435  k0004val  44391  permaxsep  45248  icof  45463  elicores  45779  dvnprodlem1  46190  dvnprodlem2  46191  dvnprodlem3  46192  stoweidlem34  46278  fourierdlem2  46353  fourierdlem3  46354  etransclem12  46490  etransclem33  46511  ovnval2b  46796  volicorescl  46797  ovncvrrp  46808  ovnsubaddlem1  46814  ovncvr2  46855  issmflem  46971  smfaddlem1  47007  smfaddlem2  47008  smflimlem1  47015  fvmptrabdm  47539  iccpval  47661  fppr  47972  grtri  48186  assintopval  48451  rngchomrnghmresALTV  48525  bigoval  48795  elbigofrcl  48796  line  48978  rrxline  48980  sphere  48993  rrxsphere  48994