Theorem rabex 2799

Description: Separation Scheme in terms of a restricted class abstraction.

Hypothesis

Ref	Expression
rabex.1	|- A e. V

Assertion

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

Distinct variable group:   x,A

Proof of Theorem rabex

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

Syntax hints:   e. wcel 994  {crab 1694  Vcvv 1857

This theorem is referenced by:  ssimaex 3879  canth 4205  inf3lema 4754  aceq6a 4887  ac6lem 4900  kmlem1 4911  zorn2lem1 4934  subval 5511  divvali 5856  nnind 6082  dfuzi 6373  uzind 6376  flval 6423  iooval 6492  ndmioo 6496  iocval 6501  icoval 6502  iccval 6503  elioo3g 6506  iccf 6528  uzval 6546  eluz2 6548  fzval 6597  elfz2 6600  elfzlem 6601  reval 6956  imval 6957  ref 6960  imf 6961  acdc3lem 7697  acdc2lem1 7700  acdc2lem2 7701  acdc5lem1 7703  acdc5lem2 7704  acdclem 7706  qdensere 7961  cnfval 7966  cnpval 7969  bcthlem12 8221  bcthlem30 8239  grpidvallem 8274  grpidval 8275  bloval 8696  hmoval 8725  ubthlem1 8787  ubthlem6 8792  ocval 9429  shsumval 9553  pjspansn 9776  pjfni 9924  nlfnval 10088  eigvecval 10102  specval 10104  cnlnadjlem4 10282  cnlnadjlem5 10283  nmopadjlei 10300  cdj3lem2 10644  elgiso 10683  limfillem1 11101  cinvlem2 11283  ordtypelem1 11427  ordtypelem6 11432  alexsublem2 11497  2ndc1stc 11538  phtpyval 12089

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-sep 2777

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-rab 1698  df-v 1858  df-in 2103  df-ss 2105

Copyright terms: Public domain