Theorem rabex 5274

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

Syntax hints:   ∈ wcel 2114  {crab 3390  Vcvv 3430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-in 3897  df-ss 3907  df-pw 4544

This theorem is referenced by:  rab2ex  5277  frminex  5601  ssimaex  6917  fvmptrabfv  6972  mptrabex  7171  fnpm  8772  inf3lema  9534  dfac2a  10041  kmlem1  10062  axcc4  10350  axdc3lem2  10362  axdc3lem4  10364  pwfseqlem1  10570  dfuzi  12609  uzval  12779  ixxval  13295  fzval  13452  bitsfval  16381  sadfval  16410  smufval  16435  phicl2  16727  hashgcdeq  16749  prmreclem4  16879  prmreclem5  16880  ismre  17541  fnmre  17542  mrisval  17585  isacs  17606  ismon  17689  isnat  17906  natffn  17908  initofn  17943  termofn  17944  initoval  17949  termoval  17950  coafval  18020  ismgmhm  18653  issubmgm  18659  ismhm  18742  issubm  18760  issubg  19091  isnsg  19119  gimfn  19225  isgim  19226  isga  19255  cntzval  19285  odfval  19496  odngen  19541  gexval  19542  isslw  19572  ablfac1a  20035  ablfac1b  20036  ablfac1c  20037  ablfac1eu  20039  ablfaclem1  20051  ablfaclem2  20052  ablfaclem3  20053  isirred  20388  rnghmfn  20408  rnghmval  20409  isrngim  20414  isrim0  20451  issubrng  20513  issubrg  20537  rrgval  20663  issdrg  20754  abvfval  20776  lssset  20917  lmimfn  21011  islmhm  21012  islmim  21047  islbs  21061  ocvval  21655  elocv  21656  isobs  21708  islinds  21797  psrval  21903  psraddcl  21926  psrvscacl  21938  psrgrp  21943  psrlmod  21946  subrgpsr  21964  mvrf  21971  mplsubrg  21991  mplmonmul  22022  mplbas2  22028  opsrval  22032  mhpval  22113  mhpmulcl  22123  mhpinvcl  22126  psdcl  22135  psdmplcl  22136  psdadd  22137  psdmul  22140  psrplusgpropd  22207  psropprmul  22209  rhmcomulmpl  22355  scmatval  22477  fncld  22995  cnfval  23206  cnpval  23209  iscnp2  23212  1stcfb  23418  kgenf  23514  xkoopn  23562  dfac14  23591  hmeofn  23730  hmeofval  23731  filunirn  23855  alexsubALTlem2  24021  ucnval  24249  iscfilu  24260  ispsmet  24277  ismet  24296  isxmet  24297  xmetunirn  24310  cncfval  24863  ishtpy  24947  isphtpy  24956  om1bas  25006  cfilfval  25239  caufval  25250  iscmet  25259  dyadmax  25573  vitalilem2  25584  vitalilem3  25585  vitalilem4  25586  itg2monolem1  25725  fncpn  25908  elcpn  25909  mdeg0  26043  mdegaddle  26047  mdegvsca  26049  uc1pval  26113  mon1pval  26115  aannenlem1  26303  aannenlem2  26304  aannenlem3  26305  vmaval  27088  sqff1o  27157  musum  27166  dchrval  27209  dchrbas  27210  leftval  27853  rightval  27854  leftf  27859  rightf  27860  precsexlem4  28214  precsexlem5  28215  tglnfn  28627  tglnunirn  28628  tglngval  28631  israg  28777  iseqlg  28947  ttgitvval  28962  ebtwntg  29063  incistruhgr  29160  usgredgleordALT  29315  vtxdun  29563  vtxdlfgrval  29567  vtxd0nedgb  29570  vtxdushgrfvedglem  29571  vtxdushgrfvedg  29572  vtxdusgr0edgnelALT  29578  1loopgrvd2  29585  usgrvd0nedg  29615  rusgrnumwrdl2  29668  ewlksfval  29683  wwlksn  29918  wspthsn  29929  iswwlksnon  29934  iswspthsnon  29937  wlknwwlksnen  29970  wwlksnexthasheq  29984  rusgrnumwlkg  30061  clwlkclwwlken  30095  clwwlkn  30109  clwwlken  30135  clwlkssizeeq  30168  clwwlknon  30173  clwwlk0on0  30175  konigsberglem5  30339  fusgreg2wsplem  30416  fusgreghash2wsp  30421  2clwwlk  30430  clwwlknonclwlknonen  30446  numclwlk1lem2  30453  numclwwlkovh0  30455  numclwwlkovq  30457  numclwwlkqhash  30458  lnoval  30836  bloval  30865  hmoval  30894  ubthlem1  30954  ubthlem2  30955  ocval  31364  eigvecval  31980  specval  31982  rabfodom  32588  fpwrelmap  32819  nsgmgc  33485  mxidlval  33534  ssmxidl  33547  rprmval  33589  evlextv  33699  mplvrpmfgalem  33701  mplvrpmga  33702  mplvrpmmhm  33703  mplvrpmrhm  33704  psrmonmul  33707  esplyfval0  33721  esplyfvaln  33731  locfinreflem  33998  rspectopn  34025  zarcls1  34027  zarclsun  34028  zarclsiin  34029  zarclsint  34030  zarclssn  34031  zarcls  34032  zartopn  34033  zar0ring  34036  zart0  34037  zarmxt1  34038  zarcmplem  34039  rhmpreimacnlem  34042  rhmpreimacn  34043  ordtconnlem1  34082  sigaex  34268  ddemeas  34394  ismbfm  34409  elunirnmbfm  34410  eulerpart  34540  ballotlem8  34695  reprval  34768  bnj110  35014  fncvm  35453  iscvm  35455  snmlval  35527  satfv1  35559  satfdm  35565  satffunlem1lem2  35599  satfv0fvfmla0  35609  satfv1fvfmla1  35619  mpstval  35731  fvray  36337  regsfromregtco  36734  icoreval  37673  fin2solem  37931  fin2so  37932  poimirlem4  37949  cnambfre  37993  istotbnd  38094  isbnd  38105  rngohomval  38289  rngoisoval  38302  idlval  38338  pridlval  38358  maxidlval  38364  lshpset  39428  lflset  39509  pats  39735  llnset  39955  lplnset  39979  lvolset  40022  isline  40189  pmapval  40207  paddval  40248  lhpset  40445  ldilset  40559  ltrnset  40568  dilsetN  40603  trnsetN  40606  diaval  41482  diafn  41484  lpolsetN  41932  lcdvadd  42047  lcdsca  42049  lcdvs  42053  mapdval  42078  mapd1o  42098  unitscyglem5  42642  psrmnd  42992  mhmcopsr  42996  mhmcoaddpsr  42997  rhmcomulpsr  42998  evlselv  43024  mhphf  43034  prjcrvval  43069  isnacs  43140  mzpclval  43161  pell1qrval  43282  pell14qrval  43284  pell1234qrval  43286  elmnc  43572  itgoval  43597  idomodle  43627  idomsubgmo  43629  k0004val  44585  permaxsep  45442  icof  45656  elicores  45971  dvnprodlem1  46382  dvnprodlem2  46383  dvnprodlem3  46384  stoweidlem34  46470  fourierdlem2  46545  fourierdlem3  46546  etransclem12  46682  etransclem33  46703  ovnval2b  46988  volicorescl  46989  ovncvrrp  47000  ovnsubaddlem1  47006  ovncvr2  47047  issmflem  47163  smfaddlem1  47199  smfaddlem2  47200  smflimlem1  47207  fvmptrabdm  47743  iccpval  47877  fppr  48204  grtri  48418  assintopval  48683  rngchomrnghmresALTV  48757  bigoval  49027  elbigofrcl  49028  line  49210  rrxline  49212  sphere  49225  rrxsphere  49226