Theorem rabex 4603

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

Hypothesis

Ref	Expression
rabex.1

Assertion

Ref	Expression
rabex

Distinct variable group:   ,

Proof of Theorem rabex

Step	Hyp	Ref	Expression
1		rabex.1	. 2
2		rabexg 4602	. 2
3	1, 2	ax-mp 5	1

Syntax hints:  e.wcel 1818  {crab 2811  cvv 3109

This theorem is referenced by:  rab2ex  4606  frminex  4864  ssimaex  5938  mptrabex  6144  fnpm  7447  inf3lema  8062  dfac2a  8531  kmlem1  8551  axcc4  8840  axdc3lem2  8852  axdc3lem4  8854  pwfseqlem1  9057  dfuzi  10978  uzval  11112  ixxval  11566  fzval  11703  bitsfval  14073  sadfval  14102  smufval  14127  phicl2  14298  prmreclem4  14437  prmreclem5  14438  ismre  14987  fnmre  14988  mrisval  15027  isacs  15048  ismon  15128  isnat  15316  natffn  15318  coafval  15391  ismhm  15968  issubm  15978  issubg  16201  isnsg  16230  gimfn  16309  isgim  16310  isga  16329  cntzval  16359  odngen  16597  gexval  16598  isslw  16628  dprdvalOLD  17036  ablfac1a  17120  ablfac1b  17121  ablfac1c  17122  ablfac1eu  17124  ablfaclem1  17136  ablfaclem2  17137  ablfaclem3  17138  isirred  17348  isrim0  17372  issubrg  17429  abvfval  17467  lssset  17580  lmimfn  17672  islmhm  17673  islmim  17708  islbs  17722  rrgval  17935  psrval  18011  psrbasOLD  18031  psraddcl  18036  psrvscacl  18046  psrgrp  18051  psrlmod  18054  psrlidmOLD  18057  psrridmOLD  18059  subrgpsr  18074  mvrf  18080  mplsubglemOLD  18095  mplsubrg  18102  mplmonmul  18126  mplbas2  18134  mplbas2OLD  18135  opsrval  18139  psrplusgpropd  18277  psropprmul  18279  ocvval  18698  elocv  18699  isobs  18751  islinds  18844  scmatval  19006  fncld  19523  cnfval  19734  cnpval  19737  iscnp2  19740  1stcfb  19946  kgenf  20042  xkoopn  20090  dfac14  20119  hmeofn  20258  hmeofval  20259  filunirn  20383  alexsubALTlem2  20548  ucnval  20780  iscfilu  20791  ispsmet  20808  ismet  20826  isxmet  20827  xmetunirn  20840  cncfval  21392  ishtpy  21472  isphtpy  21481  om1bas  21531  cfilfval  21703  caufval  21714  iscmet  21723  dyadmax  22007  vitalilem2  22018  vitalilem3  22019  vitalilem4  22020  itg2monolem1  22157  fncpn  22336  elcpn  22337  mdegleb  22464  mdeg0  22470  mdegaddle  22474  mdegvsca  22476  uc1pval  22540  mon1pval  22542  aannenlem1  22724  aannenlem2  22725  aannenlem3  22726  vmaval  23387  sqff1o  23456  musum  23467  0sgmppw  23473  dchrval  23509  dchrbas  23510  tglnfn  23934  tglnunirn  23935  tglngval  23938  israg  24074  ttgitvval  24185  ebtwntg  24285  clwlksizeeq  24852  rusgranumwlklem1  24949  rusgranumwlklem3  24951  rusgranumwlklem4  24952  rusgranumwwlkg  24959  numclwwlkovf  25081  numclwwlkovg  25087  numclwwlkovq  25099  numclwwlkqhash  25100  numclwwlkovh  25101  lnoval  25667  bloval  25696  hmoval  25725  ubthlem1  25786  ubthlem2  25787  ocval  26198  eigvecval  26815  specval  26817  rabfodom  27404  fpwrelmap  27556  locfinreflem  27843  ordtconlem1  27906  sigaex  28109  isrnsigaOLD  28112  ddemeas  28208  ismbfm  28223  elunirnmbfm  28224  eulerpart  28321  ballotlem8  28475  fncvm  28702  iscvm  28704  snmlval  28776  mpstval  28895  elgiso  29036  fvray  29791  fin2solem  30039  fin2so  30040  cnambfre  30063  istotbnd  30265  isbnd  30276  rngohomval  30367  rngoisoval  30380  idlval  30410  pridlval  30430  maxidlval  30436  isnacs  30636  mzpclval  30657  pell1qrval  30782  pell14qrval  30784  pell1234qrval  30786  mapfien2OLD  31042  elmnc  31085  itgoval  31110  issdrg  31146  idomodle  31153  idomsubgmo  31155  hashgcdeq  31158  dvnprodlem1  31743  dvnprodlem2  31744  dvnprodlem3  31745  stoweidlem34  31816  fourierdlem2  31891  fourierdlem3  31892  etransclem12  32029  etransclem33  32050  usgsizedg  32395  usgsizedgALT  32396  usgsizedgALT2  32397  fiusgedgfi  32432  fiusgedgfiALT  32433  ismgmhm  32471  issubmgm  32477  assintopval  32529  initoval  32603  termoval  32604  rnghmfn  32696  rnghmval  32697  isrngisom  32702  rngchomrnghmresOLD  32804  bnj110  33916  lshpset  34703  lflset  34784  pats  35010  llnset  35229  lplnset  35253  lvolset  35296  isline  35463  pmapval  35481  paddval  35522  lhpset  35719  ldilset  35833  ltrnset  35842  dilsetN  35878  trnsetN  35881  diaval  36759  diafn  36761  lpolsetN  37209  lcdvadd  37324  lcdsca  37326  lcdvs  37330  mapdval  37355  mapd1o  37375

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-in 3482  df-ss 3489