Theorem rabex 5297

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

Syntax hints:   ∈ wcel 2109  {crab 3408  Vcvv 3450

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 2702  ax-sep 5254

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-in 3924  df-ss 3934  df-pw 4568

This theorem is referenced by:  rab2ex  5300  frminex  5620  ssimaex  6949  fvmptrabfv  7003  mptrabex  7202  fnpm  8810  inf3lema  9584  dfac2a  10090  kmlem1  10111  axcc4  10399  axdc3lem2  10411  axdc3lem4  10413  pwfseqlem1  10618  dfuzi  12632  uzval  12802  ixxval  13321  fzval  13477  bitsfval  16400  sadfval  16429  smufval  16454  phicl2  16745  hashgcdeq  16767  prmreclem4  16897  prmreclem5  16898  ismre  17558  fnmre  17559  mrisval  17598  isacs  17619  ismon  17702  isnat  17919  natffn  17921  initofn  17956  termofn  17957  initoval  17962  termoval  17963  coafval  18033  ismgmhm  18630  issubmgm  18636  ismhm  18719  issubm  18737  issubg  19065  isnsg  19094  gimfn  19200  isgim  19201  isga  19230  cntzval  19260  odfval  19469  odngen  19514  gexval  19515  isslw  19545  ablfac1a  20008  ablfac1b  20009  ablfac1c  20010  ablfac1eu  20012  ablfaclem1  20024  ablfaclem2  20025  ablfaclem3  20026  isirred  20335  rnghmfn  20355  rnghmval  20356  isrngim  20361  isrim0OLD  20397  isrim0  20399  issubrng  20463  issubrg  20487  rrgval  20613  issdrg  20704  abvfval  20726  lssset  20846  lmimfn  20940  islmhm  20941  islmim  20976  islbs  20990  ocvval  21583  elocv  21584  isobs  21636  islinds  21725  psrval  21831  psraddcl  21854  psraddclOLD  21855  psrvscacl  21867  psrgrp  21872  psrgrpOLD  21873  psrlmod  21876  subrgpsr  21894  mvrf  21901  mplsubrg  21921  mplmonmul  21950  mplbas2  21956  opsrval  21960  mhpval  22033  mhpmulcl  22043  mhpinvcl  22046  psdcl  22055  psdmplcl  22056  psdadd  22057  psdmul  22060  psrplusgpropd  22127  psropprmul  22129  rhmcomulmpl  22276  scmatval  22398  fncld  22916  cnfval  23127  cnpval  23130  iscnp2  23133  1stcfb  23339  kgenf  23435  xkoopn  23483  dfac14  23512  hmeofn  23651  hmeofval  23652  filunirn  23776  alexsubALTlem2  23942  ucnval  24171  iscfilu  24182  ispsmet  24199  ismet  24218  isxmet  24219  xmetunirn  24232  cncfval  24788  ishtpy  24878  isphtpy  24887  om1bas  24938  cfilfval  25171  caufval  25182  iscmet  25191  dyadmax  25506  vitalilem2  25517  vitalilem3  25518  vitalilem4  25519  itg2monolem1  25658  fncpn  25842  elcpn  25843  mdeg0  25982  mdegaddle  25986  mdegvsca  25988  uc1pval  26052  mon1pval  26054  aannenlem1  26243  aannenlem2  26244  aannenlem3  26245  vmaval  27030  sqff1o  27099  musum  27108  dchrval  27152  dchrbas  27153  leftval  27778  rightval  27779  leftf  27784  rightf  27785  precsexlem4  28119  precsexlem5  28120  tglnfn  28481  tglnunirn  28482  tglngval  28485  israg  28631  iseqlg  28801  ttgitvval  28816  ebtwntg  28916  incistruhgr  29013  usgredgleordALT  29168  vtxdun  29416  vtxdlfgrval  29420  vtxd0nedgb  29423  vtxdushgrfvedglem  29424  vtxdushgrfvedg  29425  vtxdusgr0edgnelALT  29431  1loopgrvd2  29438  usgrvd0nedg  29468  rusgrnumwrdl2  29521  ewlksfval  29536  wwlksn  29774  wspthsn  29785  iswwlksnon  29790  iswspthsnon  29793  wlknwwlksnen  29826  wwlksnexthasheq  29840  rusgrnumwlkg  29914  clwlkclwwlken  29948  clwwlkn  29962  clwwlken  29988  clwlkssizeeq  30021  clwwlknon  30026  clwwlk0on0  30028  konigsberglem5  30192  fusgreg2wsplem  30269  fusgreghash2wsp  30274  2clwwlk  30283  clwwlknonclwlknonen  30299  numclwlk1lem2  30306  numclwwlkovh0  30308  numclwwlkovq  30310  numclwwlkqhash  30311  lnoval  30688  bloval  30717  hmoval  30746  ubthlem1  30806  ubthlem2  30807  ocval  31216  eigvecval  31832  specval  31834  rabfodom  32441  fpwrelmap  32663  nsgmgc  33390  mxidlval  33439  ssmxidl  33452  rprmval  33494  locfinreflem  33837  rspectopn  33864  zarcls1  33866  zarclsun  33867  zarclsiin  33868  zarclsint  33869  zarclssn  33870  zarcls  33871  zartopn  33872  zar0ring  33875  zart0  33876  zarmxt1  33877  zarcmplem  33878  rhmpreimacnlem  33881  rhmpreimacn  33882  ordtconnlem1  33921  sigaex  34107  ddemeas  34233  ismbfm  34248  elunirnmbfm  34249  eulerpart  34380  ballotlem8  34535  reprval  34608  bnj110  34855  fncvm  35251  iscvm  35253  snmlval  35325  satfv1  35357  satfdm  35363  satffunlem1lem2  35397  satfv0fvfmla0  35407  satfv1fvfmla1  35417  mpstval  35529  fvray  36136  icoreval  37348  fin2solem  37607  fin2so  37608  poimirlem4  37625  cnambfre  37669  istotbnd  37770  isbnd  37781  rngohomval  37965  rngoisoval  37978  idlval  38014  pridlval  38034  maxidlval  38040  lshpset  38978  lflset  39059  pats  39285  llnset  39506  lplnset  39530  lvolset  39573  isline  39740  pmapval  39758  paddval  39799  lhpset  39996  ldilset  40110  ltrnset  40119  dilsetN  40154  trnsetN  40157  diaval  41033  diafn  41035  lpolsetN  41483  lcdvadd  41598  lcdsca  41600  lcdvs  41604  mapdval  41629  mapd1o  41649  unitscyglem5  42194  psrmnd  42540  mhmcopsr  42544  mhmcoaddpsr  42545  rhmcomulpsr  42546  evlselv  42582  mhphf  42592  prjcrvval  42627  isnacs  42699  mzpclval  42720  pell1qrval  42841  pell14qrval  42843  pell1234qrval  42845  elmnc  43132  itgoval  43157  idomodle  43187  idomsubgmo  43189  k0004val  44146  permaxsep  45004  icof  45220  elicores  45538  dvnprodlem1  45951  dvnprodlem2  45952  dvnprodlem3  45953  stoweidlem34  46039  fourierdlem2  46114  fourierdlem3  46115  etransclem12  46251  etransclem33  46272  ovnval2b  46557  volicorescl  46558  ovncvrrp  46569  ovnsubaddlem1  46575  ovncvr2  46616  issmflem  46732  smfaddlem1  46768  smfaddlem2  46769  smflimlem1  46776  fvmptrabdm  47298  iccpval  47420  fppr  47731  grtri  47943  assintopval  48197  rngchomrnghmresALTV  48271  bigoval  48542  elbigofrcl  48543  line  48725  rrxline  48727  sphere  48740  rrxsphere  48741