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	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	rabexgfGS	$$⊢A\in V\to \left\{x\in A|\phi \right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		rabexgfGS.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		nfrab1	$$⊢\underset{\_}{Ⅎ}x\left\{x\in A|\phi \right\}$$
3	2 1	dfss2f	$$⊢\left\{x\in A|\phi \right\}\subseteq A\leftrightarrow \forall x\left(x\in \left\{x\in A|\phi \right\}\to x\in A\right)$$
4		rabidim1	$$⊢x\in \left\{x\in A|\phi \right\}\to x\in A$$
5	3 4	mpgbir	$$⊢\left\{x\in A|\phi \right\}\subseteq A$$
6		elex	$$⊢A\in V\to A\in \mathrm{V}$$
7		ssexg	$$⊢\left(\left\{x\in A|\phi \right\}\subseteq A\wedge A\in \mathrm{V}\right)\to \left\{x\in A|\phi \right\}\in \mathrm{V}$$
8	5 6 7	sylancr	$$⊢A\in V\to \left\{x\in A|\phi \right\}\in \mathrm{V}$$