Theorem rabexd

Description: Separation Scheme in terms of a restricted class abstraction, deduction form of rabex2 . (Contributed by AV, 16-Jul-2019)

	Ref	Expression
Hypotheses	rabexd.1	|- B = { x e. A | ps }
	rabexd.2	|- ( ph -> A e. V )
Assertion	rabexd	|- ( ph -> B e. _V )

Proof

Step	Hyp	Ref	Expression
1		rabexd.1	|- B = { x e. A | ps }
2		rabexd.2	|- ( ph -> A e. V )
3		rabexg	|- ( A e. V -> { x e. A | ps } e. _V )
4	2 3	syl	|- ( ph -> { x e. A | ps } e. _V )
5	1 4	eqeltrid	|- ( ph -> B e. _V )