Theorem rabex 5257

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

Syntax hints:   ∈ wcel 2107  {crab 3069  Vcvv 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-sep 5224

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-in 3895  df-ss 3905

This theorem is referenced by:  rab2ex  5260  frminex  5570  ssimaex  6862  fvmptrabfv  6915  mptrabex  7110  fnpm  8632  inf3lema  9391  dfac2a  9894  kmlem1  9915  axcc4  10204  axdc3lem2  10216  axdc3lem4  10218  pwfseqlem1  10423  dfuzi  12420  uzval  12593  ixxval  13096  fzval  13250  bitsfval  16139  sadfval  16168  smufval  16193  phicl2  16478  hashgcdeq  16499  prmreclem4  16629  prmreclem5  16630  ismre  17308  fnmre  17309  mrisval  17348  isacs  17369  ismon  17454  isnat  17672  natffn  17674  initofn  17711  termofn  17712  initoval  17717  termoval  17718  coafval  17788  ismhm  18441  issubm  18451  issubg  18764  isnsg  18792  gimfn  18886  isgim  18887  isga  18906  cntzval  18936  odfval  19149  odngen  19191  gexval  19192  isslw  19222  ablfac1a  19681  ablfac1b  19682  ablfac1c  19683  ablfac1eu  19685  ablfaclem1  19697  ablfaclem2  19698  ablfaclem3  19699  isirred  19950  isrim0  19976  issubrg  20033  issdrg  20072  abvfval  20087  lssset  20204  lmimfn  20297  islmhm  20298  islmim  20333  islbs  20347  rrgval  20567  ocvval  20881  elocv  20882  isobs  20936  islinds  21025  psrval  21127  psraddcl  21161  psrvscacl  21171  psrgrp  21176  psrlmod  21179  subrgpsr  21197  mvrf  21202  mplsubrg  21220  mplmonmul  21246  mplbas2  21252  opsrval  21256  mhpval  21339  mhpmulcl  21348  mhpinvcl  21351  psrplusgpropd  21416  psropprmul  21418  scmatval  21662  fncld  22182  cnfval  22393  cnpval  22396  iscnp2  22399  1stcfb  22605  kgenf  22701  xkoopn  22749  dfac14  22778  hmeofn  22917  hmeofval  22918  filunirn  23042  alexsubALTlem2  23208  ucnval  23438  iscfilu  23449  ispsmet  23466  ismet  23485  isxmet  23486  xmetunirn  23499  cncfval  24060  ishtpy  24144  isphtpy  24153  om1bas  24203  cfilfval  24437  caufval  24448  iscmet  24457  dyadmax  24771  vitalilem2  24782  vitalilem3  24783  vitalilem4  24784  itg2monolem1  24924  fncpn  25106  elcpn  25107  mdeg0  25244  mdegaddle  25248  mdegvsca  25250  uc1pval  25313  mon1pval  25315  aannenlem1  25497  aannenlem2  25498  aannenlem3  25499  vmaval  26271  sqff1o  26340  musum  26349  dchrval  26391  dchrbas  26392  tglnfn  26917  tglnunirn  26918  tglngval  26921  israg  27067  iseqlg  27237  ttgitvval  27258  ebtwntg  27359  incistruhgr  27458  usgredgleordALT  27610  vtxdun  27857  vtxdlfgrval  27861  vtxd0nedgb  27864  vtxdushgrfvedglem  27865  vtxdushgrfvedg  27866  vtxdusgr0edgnelALT  27872  1loopgrvd2  27879  usgrvd0nedg  27909  rusgrnumwrdl2  27962  ewlksfval  27977  wwlksn  28211  wspthsn  28222  iswwlksnon  28227  iswspthsnon  28230  wlknwwlksnen  28263  wwlksnexthasheq  28277  rusgrnumwlkg  28351  clwlkclwwlken  28385  clwwlkn  28399  clwwlken  28425  clwlkssizeeq  28458  clwwlknon  28463  clwwlk0on0  28465  konigsberglem5  28629  fusgreg2wsplem  28706  fusgreghash2wsp  28711  2clwwlk  28720  clwwlknonclwlknonen  28736  numclwlk1lem2  28743  numclwwlkovh0  28745  numclwwlkovq  28747  numclwwlkqhash  28748  lnoval  29123  bloval  29152  hmoval  29181  ubthlem1  29241  ubthlem2  29242  ocval  29651  eigvecval  30267  specval  30269  rabfodom  30860  fpwrelmap  31077  nsgmgc  31606  mxidlval  31642  ssmxidl  31651  rprmval  31673  locfinreflem  31799  rspectopn  31826  zarcls1  31828  zarclsun  31829  zarclsiin  31830  zarclsint  31831  zarclssn  31832  zarcls  31833  zartopn  31834  zar0ring  31837  zart0  31838  zarmxt1  31839  zarcmplem  31840  rhmpreimacnlem  31843  rhmpreimacn  31844  ordtconnlem1  31883  sigaex  32087  ddemeas  32213  ismbfm  32228  elunirnmbfm  32229  eulerpart  32358  ballotlem8  32512  reprval  32599  bnj110  32847  fncvm  33228  iscvm  33230  snmlval  33302  satfv1  33334  satfdm  33340  satffunlem1lem2  33374  satfv0fvfmla0  33384  satfv1fvfmla1  33394  mpstval  33506  leftval  34056  rightval  34057  leftf  34058  rightf  34059  fvray  34452  icoreval  35533  fin2solem  35772  fin2so  35773  poimirlem4  35790  cnambfre  35834  istotbnd  35936  isbnd  35947  rngohomval  36131  rngoisoval  36144  idlval  36180  pridlval  36200  maxidlval  36206  lshpset  36999  lflset  37080  pats  37306  llnset  37526  lplnset  37550  lvolset  37593  isline  37760  pmapval  37778  paddval  37819  lhpset  38016  ldilset  38130  ltrnset  38139  dilsetN  38174  trnsetN  38177  diaval  39053  diafn  39055  lpolsetN  39503  lcdvadd  39618  lcdsca  39620  lcdvs  39624  mapdval  39649  mapd1o  39669  selvval2lem4  40235  mhphf  40292  prjcrvval  40476  isnacs  40533  mzpclval  40554  pell1qrval  40675  pell14qrval  40677  pell1234qrval  40679  elmnc  40968  itgoval  40993  idomodle  41028  idomsubgmo  41030  k0004val  41767  icof  42766  elicores  43078  dvnprodlem1  43494  dvnprodlem2  43495  dvnprodlem3  43496  stoweidlem34  43582  fourierdlem2  43657  fourierdlem3  43658  etransclem12  43794  etransclem33  43815  ovnval2b  44097  volicorescl  44098  ovncvrrp  44109  ovnsubaddlem1  44115  ovncvr2  44156  issmflem  44272  smfaddlem1  44308  smfaddlem2  44309  smflimlem1  44316  fvmptrabdm  44796  iccpval  44878  fppr  45189  ismgmhm  45348  issubmgm  45354  assintopval  45410  rnghmfn  45459  rnghmval  45460  isrngisom  45465  rngchomrnghmresALTV  45565  bigoval  45906  elbigofrcl  45907  line  46089  rrxline  46091  sphere  46104  rrxsphere  46105