Theorem rabexgfGS

Description: Separation Scheme in terms of a restricted class abstraction. To be removed in profit of Glauco's equivalent version. (Contributed by Thierry Arnoux, 11-May-2017)

	Ref	Expression
Hypothesis	rabexgfGS.1	|- F/_ x A
Assertion	rabexgfGS	|- ( A e. V -> { x e. A | ph } e. _V )

Proof

Step	Hyp	Ref	Expression
1		rabexgfGS.1	|- F/_ x A
2		nfrab1	|- F/_ x { x e. A | ph }
3	2 1	dfss2f	|- ( { x e. A | ph } C_ A <-> A. x ( x e. { x e. A | ph } -> x e. A ) )
4		rabidim1	|- ( x e. { x e. A | ph } -> x e. A )
5	3 4	mpgbir	|- { x e. A | ph } C_ A
6		elex	|- ( A e. V -> A e. _V )
7		ssexg	|- ( ( { x e. A | ph } C_ A /\ A e. _V ) -> { x e. A | ph } e. _V )
8	5 6 7	sylancr	|- ( A e. V -> { x e. A | ph } e. _V )