Theorem rabex 2730

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 2729	. 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 960  {crab 1651  Vcvv 1814

This theorem is referenced by:  ssimaex 3774  canth 3913  inf3lema 4618  aceq6a 4751  ac6lem 4764  kmlem1 4775  zorn2lem1 4798  subvalt 5369  divval 5716  nnind 5939  dfuz 6204  uzind 6207  flvalt 6227  ioovalt 6367  ndmioo 6371  iocvalt 6376  icovalt 6377  iccvalt 6378  elioo3g 6381  iccf 6402  uzvalt 6420  eluz2t 6422  fzvalt 6470  elfz2t 6473  elfzlem 6474  revalt 6756  imvalt 6757  ref 6760  imf 6761  acdc3lem 7487  acdc2lem1 7489  acdc2lem2 7490  acdc5lem1 7492  acdc5lem2 7493  acdclem 7495  qdensere 7748  cnfval 7753  cnpval 7756  bcthlem12 8007  bcthlem30 8025  0vfval 8221  bloval 8437  hmoval 8466  ubthlem1 8525  ubthlem6 8530  ocvalt 9148  shsumvalt 9272  pjspansnt 9495  pjfn 9641  nlfnvalt 9803  eigvecvalt 9817  specvalt 9819  cnlnadjlem4 9998  cnlnadjlem5 9999  nmopadjle 10016  cdj3lem2 10357  elgiso 10393  limfillem1OLD 10578

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-sep 2708

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-rab 1655  df-v 1815  df-in 2054  df-ss 2056

Copyright terms: Public domain