Theorem rabex 5089

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

Syntax hints:   ∈ wcel 2048  {crab 3089  Vcvv 3412

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2747  ax-sep 5058

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2756  df-cleq 2768  df-clel 2843  df-nfc 2915  df-rab 3094  df-v 3414  df-in 3835  df-ss 3842

This theorem is referenced by:  rab2ex  5092  frminex  5384  ssimaex  6574  fvmptrabfv  6622  mptrabex  6812  fnpm  8210  inf3lema  8877  dfac2a  9345  kmlem1  9366  axcc4  9655  axdc3lem2  9667  axdc3lem4  9669  pwfseqlem1  9874  dfuzi  11883  uzval  12057  ixxval  12559  fzval  12707  bitsfval  15626  sadfval  15655  smufval  15680  phicl2  15955  hashgcdeq  15976  prmreclem4  16105  prmreclem5  16106  ismre  16713  fnmre  16714  mrisval  16753  isacs  16774  ismon  16855  isnat  17069  natffn  17071  initoval  17109  termoval  17110  coafval  17176  ismhm  17799  issubm  17809  issubg  18057  isnsg  18086  gimfn  18166  isgim  18167  isga  18186  cntzval  18216  odfval  18416  odngen  18457  gexval  18458  isslw  18488  ablfac1a  18935  ablfac1b  18936  ablfac1c  18937  ablfac1eu  18939  ablfaclem1  18951  ablfaclem2  18952  ablfaclem3  18953  isirred  19166  isrim0  19192  issubrg  19252  issdrg  19290  abvfval  19305  lssset  19421  lmimfn  19514  islmhm  19515  islmim  19550  islbs  19564  rrgval  19775  psrval  19850  psraddcl  19871  psrvscacl  19881  psrgrp  19886  psrlmod  19889  subrgpsr  19907  mvrf  19912  mplsubrg  19928  mplmonmul  19952  mplbas2  19958  opsrval  19962  mhpval  20033  psrplusgpropd  20101  psropprmul  20103  ocvval  20507  elocv  20508  isobs  20560  islinds  20649  scmatval  20811  fncld  21328  cnfval  21539  cnpval  21542  iscnp2  21545  1stcfb  21751  kgenf  21847  xkoopn  21895  dfac14  21924  hmeofn  22063  hmeofval  22064  filunirn  22188  alexsubALTlem2  22354  ucnval  22583  iscfilu  22594  ispsmet  22611  ismet  22630  isxmet  22631  xmetunirn  22644  cncfval  23193  ishtpy  23273  isphtpy  23282  om1bas  23332  cfilfval  23564  caufval  23575  iscmet  23584  dyadmax  23896  vitalilem2  23907  vitalilem3  23908  vitalilem4  23909  itg2monolem1  24048  fncpn  24227  elcpn  24228  mdegleb  24355  mdeg0  24361  mdegaddle  24365  mdegvsca  24367  uc1pval  24430  mon1pval  24432  aannenlem1  24614  aannenlem2  24615  aannenlem3  24616  vmaval  25386  sqff1o  25455  musum  25464  dchrval  25506  dchrbas  25507  tglnfn  26029  tglnunirn  26030  tglngval  26033  israg  26179  iseqlg  26350  ttgitvval  26365  ebtwntg  26465  incistruhgr  26561  usgredgleordALT  26713  vtxdun  26960  vtxdlfgrval  26964  vtxd0nedgb  26967  vtxdushgrfvedglem  26968  vtxdushgrfvedg  26969  vtxdusgr0edgnelALT  26975  1loopgrvd2  26982  usgrvd0nedg  27012  rusgrnumwrdl2  27065  ewlksfval  27080  wwlksn  27317  wspthsn  27328  iswwlksnon  27333  iswspthsnon  27336  wlknwwlksnen  27370  wwlksnexthasheq  27394  wwlksnexthasheqOLD  27395  rusgrnumwlkg  27478  clwlkclwwlken  27520  clwlkclwwlkenOLD  27521  clwwlkn  27535  clwwlken  27568  clwwlkenOLD  27569  clwlkssizeeq  27606  clwlkssizeeqOLD  27607  clwwlknon  27612  clwwlk0on0  27614  konigsberglem5  27782  fusgreg2wsplem  27861  fusgreghash2wsp  27866  2clwwlk  27878  clwwlknonclwlknonen  27906  clwwlknonclwlknonenOLD  27907  numclwlk1lem2  27917  numclwwlkovh0  27919  numclwwlkovq  27921  numclwwlkqhash  27922  lnoval  28300  bloval  28329  hmoval  28358  ubthlem1  28419  ubthlem2  28420  ocval  28832  eigvecval  29448  specval  29450  rabfodom  30039  fpwrelmap  30215  locfinreflem  30739  ordtconnlem1  30802  sigaex  31004  isrnsigaOLD  31007  ddemeas  31131  ismbfm  31146  elunirnmbfm  31147  eulerpart  31276  ballotlem8  31431  reprval  31520  bnj110  31768  fncvm  32079  iscvm  32081  snmlval  32153  mpstval  32272  fvray  33093  icoreval  34041  fin2solem  34297  fin2so  34298  poimirlem4  34315  cnambfre  34359  istotbnd  34467  isbnd  34478  rngohomval  34662  rngoisoval  34675  idlval  34711  pridlval  34731  maxidlval  34737  lshpset  35537  lflset  35618  pats  35844  llnset  36064  lplnset  36088  lvolset  36131  isline  36298  pmapval  36316  paddval  36357  lhpset  36554  ldilset  36668  ltrnset  36677  dilsetN  36712  trnsetN  36715  diaval  37591  diafn  37593  lpolsetN  38041  lcdvadd  38156  lcdsca  38158  lcdvs  38162  mapdval  38187  mapd1o  38207  isnacs  38674  mzpclval  38695  pell1qrval  38817  pell14qrval  38819  pell1234qrval  38821  elmnc  39110  itgoval  39135  idomodle  39170  idomsubgmo  39172  k0004val  39841  icof  40886  elicores  41219  dvnprodlem1  41640  dvnprodlem2  41641  dvnprodlem3  41642  stoweidlem34  41729  fourierdlem2  41804  fourierdlem3  41805  etransclem12  41941  etransclem33  41962  ovnval2b  42244  volicorescl  42245  ovncvrrp  42256  ovnsubaddlem1  42262  ovncvr2  42303  issmflem  42414  smfaddlem1  42449  smfaddlem2  42450  smflimlem1  42457  fvmptrabdm  42877  iccpval  42926  fppr  43233  ismgmhm  43392  issubmgm  43398  assintopval  43450  rnghmfn  43499  rnghmval  43500  isrngisom  43505  rngchomrnghmresALTV  43605  bigoval  43951  elbigofrcl  43952  line  44061  rrxline  44063  sphere  44076  rrxsphere  44077