Theorem rabex 4813

Description: Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 19-Jul-1996.)

Hypothesis

Ref	Expression
rabex.1	|- A e. _V

Assertion

Ref	Expression
rabex	|- { x e. A | ph } e. _V

Distinct variable group:   x, A

Allowed substitution hint:   ph( x)

Proof of Theorem rabex

Step	Hyp	Ref	Expression
1		rabex.1	. 2 |- A e. _V
2		rabexg 4812	. 2 |- ( A e. _V -> { x e. A | ph } e. _V )
3	1, 2	ax-mp 5	1 |- { x e. A | ph } e. _V

Syntax hints:   e. wcel 1990   {crab 2916   _Vcvv 3200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-in 3581  df-ss 3588

This theorem is referenced by:  rab2ex  4816  rab2exOLD  4818  frminex  5094  ssimaex  6263  mptrabex  6488  mptrabexOLD  6489  fnpm  7865  inf3lema  8521  dfac2a  8952  kmlem1  8972  axcc4  9261  axdc3lem2  9273  axdc3lem4  9275  pwfseqlem1  9480  dfuzi  11468  uzval  11689  ixxval  12183  fzval  12328  bitsfval  15145  sadfval  15174  smufval  15199  phicl2  15473  hashgcdeq  15494  prmreclem4  15623  prmreclem5  15624  ismre  16250  fnmre  16251  mrisval  16290  isacs  16312  ismon  16393  isnat  16607  natffn  16609  initoval  16647  termoval  16648  coafval  16714  ismhm  17337  issubm  17347  issubg  17594  isnsg  17623  gimfn  17703  isgim  17704  isga  17724  cntzval  17754  odngen  17992  gexval  17993  isslw  18023  ablfac1a  18468  ablfac1b  18469  ablfac1c  18470  ablfac1eu  18472  ablfaclem1  18484  ablfaclem2  18485  ablfaclem3  18486  isirred  18699  isrim0  18723  issubrg  18780  abvfval  18818  lssset  18934  lmimfn  19026  islmhm  19027  islmim  19062  islbs  19076  rrgval  19287  psrval  19362  psraddcl  19383  psrvscacl  19393  psrgrp  19398  psrlmod  19401  subrgpsr  19419  mvrf  19424  mplsubrg  19440  mplmonmul  19464  mplbas2  19470  opsrval  19474  psrplusgpropd  19606  psropprmul  19608  ocvval  20011  elocv  20012  isobs  20064  islinds  20148  scmatval  20310  fncld  20826  cnfval  21037  cnpval  21040  iscnp2  21043  1stcfb  21248  kgenf  21344  xkoopn  21392  dfac14  21421  hmeofn  21560  hmeofval  21561  filunirn  21686  alexsubALTlem2  21852  ucnval  22081  iscfilu  22092  ispsmet  22109  ismet  22128  isxmet  22129  xmetunirn  22142  cncfval  22691  ishtpy  22771  isphtpy  22780  om1bas  22831  cfilfval  23062  caufval  23073  iscmet  23082  dyadmax  23366  vitalilem2  23378  vitalilem3  23379  vitalilem4  23380  itg2monolem1  23517  fncpn  23696  elcpn  23697  mdegleb  23824  mdeg0  23830  mdegaddle  23834  mdegvsca  23836  uc1pval  23899  mon1pval  23901  aannenlem1  24083  aannenlem2  24084  aannenlem3  24085  vmaval  24839  sqff1o  24908  musum  24917  0sgmppw  24923  dchrval  24959  dchrbas  24960  tglnfn  25442  tglnunirn  25443  tglngval  25446  israg  25592  iseqlg  25747  ttgitvval  25762  ebtwntg  25862  incistruhgr  25974  usgredgleordALT  26126  uvtxaval  26287  vtxdun  26377  vtxdlfgrval  26381  vtxd0nedgb  26384  vtxdushgrfvedglem  26385  vtxdushgrfvedg  26386  vtxdusgr0edgnelALT  26392  1loopgrvd2  26399  usgrvd0nedg  26429  vtxdginducedm1lem4  26438  rusgrnumwrdl2  26482  ewlksfval  26497  wwlksn  26729  wspthsn  26735  iswwlksnon  26740  iswspthsnon  26741  wwlksnexthasheq  26798  wwlks2onv  26847  rusgrnumwlkg  26872  clwwlksn  26881  clwlkssizeeq  26971  konigsberglem5  27118  fusgreg2wsplem  27197  fusgreghash2wsp  27202  numclwwlkovf  27213  numclwwlkovg  27220  numclwwlkovq  27232  numclwwlkqhash  27233  numclwwlkovh  27234  lnoval  27607  bloval  27636  hmoval  27665  ubthlem1  27726  ubthlem2  27727  ocval  28139  eigvecval  28755  specval  28757  rabfodom  29344  fpwrelmap  29508  locfinreflem  29907  ordtconnlem1  29970  sigaex  30172  isrnsigaOLD  30175  ddemeas  30299  ismbfm  30314  elunirnmbfm  30315  eulerpart  30444  ballotlem8  30598  reprval  30688  bnj110  30928  fncvm  31239  iscvm  31241  snmlval  31313  mpstval  31432  fvray  32248  icoreval  33201  fin2solem  33395  fin2so  33396  poimirlem4  33413  cnambfre  33458  istotbnd  33568  isbnd  33579  rngohomval  33763  rngoisoval  33776  idlval  33812  pridlval  33832  maxidlval  33838  lshpset  34265  lflset  34346  pats  34572  llnset  34791  lplnset  34815  lvolset  34858  isline  35025  pmapval  35043  paddval  35084  lhpset  35281  ldilset  35395  ltrnset  35404  dilsetN  35440  trnsetN  35443  diaval  36321  diafn  36323  lpolsetN  36771  lcdvadd  36886  lcdsca  36888  lcdvs  36892  mapdval  36917  mapd1o  36937  isnacs  37267  mzpclval  37288  pell1qrval  37410  pell14qrval  37412  pell1234qrval  37414  elmnc  37706  itgoval  37731  issdrg  37767  idomodle  37774  idomsubgmo  37776  k0004val  38448  icof  39411  elicores  39760  dvnprodlem1  40161  dvnprodlem2  40162  dvnprodlem3  40163  stoweidlem34  40251  fourierdlem2  40326  fourierdlem3  40327  etransclem12  40463  etransclem33  40484  ovnval2b  40766  volicorescl  40767  ovncvrrp  40778  ovnsubaddlem1  40784  ovncvr2  40825  issmflem  40936  smfaddlem1  40971  smfaddlem2  40972  smflimlem1  40979  iccpval  41351  ismgmhm  41783  issubmgm  41789  assintopval  41841  rnghmfn  41890  rnghmval  41891  isrngisom  41896  rngchomrnghmresALTV  41996  bigoval  42343  elbigofrcl  42344