Theorem rabex 2720

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 2719	. 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 956  {crab 1645  Vcvv 1807

This theorem is referenced by:  ssimaex 3759  canth 3898  inf3lema 4589  aceq6a 4721  ac6lem 4734  kmlem1 4745  zorn2lem1 4768  subvalt 5337  divval 5681  nnind 5893  dfuz 6158  uzind 6161  flvalt 6181  ioovalt 6311  ndmioo 6315  iocvalt 6320  icovalt 6321  iccvalt 6322  elioo3g 6325  iccf 6342  uzvalt 6359  eluz2t 6361  fzvalt 6409  elfz2t 6412  elfzlem 6413  revalt 6694  imvalt 6695  ref 6698  imf 6699  acdc3lem 7436  acdc2lem1 7438  acdc2lem2 7439  acdc5lem1 7441  acdc5lem2 7442  acdclem 7444  qdensere 7701  cnfval 7706  cnpval 7709  bcthlem12 7960  bcthlem30 7978  0vfval 8177  bloval 8386  hmoval 8414  ubthlem1 8473  ubthlem6 8478  circgrpOLD 8677  ocvalt 9092  shsumvalt 9215  pjspansnt 9440  pjfn 9586  nlfnvalt 9748  eigvecvalt 9762  specvalt 9764  cnlnadjlem4 9941  cnlnadjlem5 9942  nmopadjle 9959  cdj3lem2 10296  elgiso 10332

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-rab 1649  df-v 1808  df-in 2047  df-ss 2049

Copyright terms: Public domain