Theorem rabex 5289

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

Syntax hints:   ∈ wcel 2109  {crab 3402  Vcvv 3444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-in 3918  df-ss 3928  df-pw 4561

This theorem is referenced by:  rab2ex  5292  frminex  5610  ssimaex  6928  fvmptrabfv  6982  mptrabex  7181  fnpm  8784  inf3lema  9553  dfac2a  10059  kmlem1  10080  axcc4  10368  axdc3lem2  10380  axdc3lem4  10382  pwfseqlem1  10587  dfuzi  12601  uzval  12771  ixxval  13290  fzval  13446  bitsfval  16369  sadfval  16398  smufval  16423  phicl2  16714  hashgcdeq  16736  prmreclem4  16866  prmreclem5  16867  ismre  17527  fnmre  17528  mrisval  17567  isacs  17588  ismon  17671  isnat  17888  natffn  17890  initofn  17925  termofn  17926  initoval  17931  termoval  17932  coafval  18002  ismgmhm  18599  issubmgm  18605  ismhm  18688  issubm  18706  issubg  19034  isnsg  19063  gimfn  19169  isgim  19170  isga  19199  cntzval  19229  odfval  19438  odngen  19483  gexval  19484  isslw  19514  ablfac1a  19977  ablfac1b  19978  ablfac1c  19979  ablfac1eu  19981  ablfaclem1  19993  ablfaclem2  19994  ablfaclem3  19995  isirred  20304  rnghmfn  20324  rnghmval  20325  isrngim  20330  isrim0OLD  20366  isrim0  20368  issubrng  20432  issubrg  20456  rrgval  20582  issdrg  20673  abvfval  20695  lssset  20815  lmimfn  20909  islmhm  20910  islmim  20945  islbs  20959  ocvval  21552  elocv  21553  isobs  21605  islinds  21694  psrval  21800  psraddcl  21823  psraddclOLD  21824  psrvscacl  21836  psrgrp  21841  psrgrpOLD  21842  psrlmod  21845  subrgpsr  21863  mvrf  21870  mplsubrg  21890  mplmonmul  21919  mplbas2  21925  opsrval  21929  mhpval  22002  mhpmulcl  22012  mhpinvcl  22015  psdcl  22024  psdmplcl  22025  psdadd  22026  psdmul  22029  psrplusgpropd  22096  psropprmul  22098  rhmcomulmpl  22245  scmatval  22367  fncld  22885  cnfval  23096  cnpval  23099  iscnp2  23102  1stcfb  23308  kgenf  23404  xkoopn  23452  dfac14  23481  hmeofn  23620  hmeofval  23621  filunirn  23745  alexsubALTlem2  23911  ucnval  24140  iscfilu  24151  ispsmet  24168  ismet  24187  isxmet  24188  xmetunirn  24201  cncfval  24757  ishtpy  24847  isphtpy  24856  om1bas  24907  cfilfval  25140  caufval  25151  iscmet  25160  dyadmax  25475  vitalilem2  25486  vitalilem3  25487  vitalilem4  25488  itg2monolem1  25627  fncpn  25811  elcpn  25812  mdeg0  25951  mdegaddle  25955  mdegvsca  25957  uc1pval  26021  mon1pval  26023  aannenlem1  26212  aannenlem2  26213  aannenlem3  26214  vmaval  26999  sqff1o  27068  musum  27077  dchrval  27121  dchrbas  27122  leftval  27747  rightval  27748  leftf  27753  rightf  27754  precsexlem4  28088  precsexlem5  28089  tglnfn  28450  tglnunirn  28451  tglngval  28454  israg  28600  iseqlg  28770  ttgitvval  28785  ebtwntg  28885  incistruhgr  28982  usgredgleordALT  29137  vtxdun  29385  vtxdlfgrval  29389  vtxd0nedgb  29392  vtxdushgrfvedglem  29393  vtxdushgrfvedg  29394  vtxdusgr0edgnelALT  29400  1loopgrvd2  29407  usgrvd0nedg  29437  rusgrnumwrdl2  29490  ewlksfval  29505  wwlksn  29740  wspthsn  29751  iswwlksnon  29756  iswspthsnon  29759  wlknwwlksnen  29792  wwlksnexthasheq  29806  rusgrnumwlkg  29880  clwlkclwwlken  29914  clwwlkn  29928  clwwlken  29954  clwlkssizeeq  29987  clwwlknon  29992  clwwlk0on0  29994  konigsberglem5  30158  fusgreg2wsplem  30235  fusgreghash2wsp  30240  2clwwlk  30249  clwwlknonclwlknonen  30265  numclwlk1lem2  30272  numclwwlkovh0  30274  numclwwlkovq  30276  numclwwlkqhash  30277  lnoval  30654  bloval  30683  hmoval  30712  ubthlem1  30772  ubthlem2  30773  ocval  31182  eigvecval  31798  specval  31800  rabfodom  32407  fpwrelmap  32629  nsgmgc  33356  mxidlval  33405  ssmxidl  33418  rprmval  33460  locfinreflem  33803  rspectopn  33830  zarcls1  33832  zarclsun  33833  zarclsiin  33834  zarclsint  33835  zarclssn  33836  zarcls  33837  zartopn  33838  zar0ring  33841  zart0  33842  zarmxt1  33843  zarcmplem  33844  rhmpreimacnlem  33847  rhmpreimacn  33848  ordtconnlem1  33887  sigaex  34073  ddemeas  34199  ismbfm  34214  elunirnmbfm  34215  eulerpart  34346  ballotlem8  34501  reprval  34574  bnj110  34821  fncvm  35217  iscvm  35219  snmlval  35291  satfv1  35323  satfdm  35329  satffunlem1lem2  35363  satfv0fvfmla0  35373  satfv1fvfmla1  35383  mpstval  35495  fvray  36102  icoreval  37314  fin2solem  37573  fin2so  37574  poimirlem4  37591  cnambfre  37635  istotbnd  37736  isbnd  37747  rngohomval  37931  rngoisoval  37944  idlval  37980  pridlval  38000  maxidlval  38006  lshpset  38944  lflset  39025  pats  39251  llnset  39472  lplnset  39496  lvolset  39539  isline  39706  pmapval  39724  paddval  39765  lhpset  39962  ldilset  40076  ltrnset  40085  dilsetN  40120  trnsetN  40123  diaval  40999  diafn  41001  lpolsetN  41449  lcdvadd  41564  lcdsca  41566  lcdvs  41570  mapdval  41595  mapd1o  41615  unitscyglem5  42160  psrmnd  42506  mhmcopsr  42510  mhmcoaddpsr  42511  rhmcomulpsr  42512  evlselv  42548  mhphf  42558  prjcrvval  42593  isnacs  42665  mzpclval  42686  pell1qrval  42807  pell14qrval  42809  pell1234qrval  42811  elmnc  43098  itgoval  43123  idomodle  43153  idomsubgmo  43155  k0004val  44112  permaxsep  44970  icof  45186  elicores  45504  dvnprodlem1  45917  dvnprodlem2  45918  dvnprodlem3  45919  stoweidlem34  46005  fourierdlem2  46080  fourierdlem3  46081  etransclem12  46217  etransclem33  46238  ovnval2b  46523  volicorescl  46524  ovncvrrp  46535  ovnsubaddlem1  46541  ovncvr2  46582  issmflem  46698  smfaddlem1  46734  smfaddlem2  46735  smflimlem1  46742  fvmptrabdm  47267  iccpval  47389  fppr  47700  grtri  47912  assintopval  48166  rngchomrnghmresALTV  48240  bigoval  48511  elbigofrcl  48512  line  48694  rrxline  48696  sphere  48709  rrxsphere  48710