Theorem rabexg 4602

Description: Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 23-Oct-1999.)

Assertion

Ref	Expression
rabexg

Distinct variable group:   ,

Proof of Theorem rabexg

Step	Hyp	Ref	Expression
1		ssrab2 3584	. 2
2		ssexg 4598	. 2
3	1, 2	mpan 670	1

Syntax hints:  ->wi 4  e.wcel 1818  {crab 2811  cvv 3109  C_wss 3475

This theorem is referenced by:  rabex  4603  rabexd  4604  class2set  4619  exse  4848  elfvmptrab1  5976  elovmpt2rab  6521  elovmpt2rab1  6522  ovmpt3rabdm  6535  elovmpt3rab1  6536  suppval  6920  mpt2xopoveq  6966  wdom2d  8027  scottex  8324  tskwe  8352  fin1a2lem12  8812  hashbclem  12501  wrdnfi  12574  wrd2f1tovbij  12898  hashdvds  14305  hashbcval  14520  brric  17393  psrass1lem  18029  psrcom  18064  dmatval  18994  cpmat  19210  fctop  19505  cctop  19507  ppttop  19508  epttop  19510  cldval  19524  neif  19601  neival  19603  neiptoptop  19632  neiptopnei  19633  ordtbaslem  19689  ordtbas2  19692  ordtopn1  19695  ordtopn2  19696  ordtrest2lem  19704  cmpsublem  19899  kgenval  20036  qtopval  20196  kqfval  20224  ordthmeolem  20302  elmptrab  20328  fbssfi  20338  fgval  20371  flimval  20464  flimfnfcls  20529  ptcmplem2  20553  ptcmplem3  20554  tsmsfbas  20626  eltsms  20631  utopval  20735  blvalps  20888  blval  20889  minveclem3b  21843  minveclem3  21844  minveclem4  21847  fiusgraedgfi  24407  nbgraop  24423  isuvtx  24488  wwlk  24681  wwlkn  24682  wwlkextbij  24733  wwlkexthasheq  24734  clwwlk  24766  clwwlkn  24767  2wlkonot  24865  2spthonot  24866  2wlksot  24867  2spthsot  24868  vdgrf  24898  vdgrun  24901  vdusgraval  24907  hashnbgravdg  24913  usgravd0nedg  24918  rusgranumwwlkl1  24946  vdn0frgrav2  25023  vdgn0frgrav2  25024  vdn1frgrav2  25025  vdgn1frgrav2  25026  frgrawopreglem1  25044  usg2spot2nb  25065  usgreg2spot  25067  2spotmdisj  25068  usgreghash2spot  25069  rabfodom  27404  ordtrest2NEWlem  27904  hasheuni  28091  sigaval  28110  ddemeas  28208  braew  28214  imambfm  28233  iscvm  28704  cvmsval  28711  fnessref  30175  indexa  30224  supex2g  30228  cnfex  31403  stoweidlem26  31808  stoweidlem31  31813  stoweidlem34  31816  stoweidlem46  31828  stoweidlem59  31841  dmatALTbas  33002  lcoop  33012

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