Theorem rabexg 2714

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

Assertion

Ref	Expression
rabexg	|- (A e. B -> {x e. A | ph} e. V)

Distinct variable group:   x,A

Proof of Theorem rabexg

Step	Hyp	Ref	Expression
1		ssrab2 2121	. 2 |- {x e. A | ph} (_ A
2		ssexg 2711	. 2 |- (({x e. A | ph} (_ A /\ A e. B) -> {x e. A | ph} e. V)
3	1, 2	mpan 693	1 |- (A e. B -> {x e. A | ph} e. V)

Syntax hints:   -> wi 3   e. wcel 955  {crab 1640  Vcvv 1802   (_ wss 2037

This theorem is referenced by:  rabex 2715  class2set 2724  abssexg 2737  scottex 4688  lbinfm 5995  ntrval 7618  blval 7777  blrn 7781  grpidval 7992  grpinvval 8001  grpinvf 8014  spwval2 8577  pjvalt 9154  fiv 10374  fgsb 10444  fgsb2 10449  isfuna 10592

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-rab 1644  df-v 1803  df-in 2041  df-ss 2043

Copyright terms: Public domain