Theorem rabex2

Description: Separation Scheme in terms of a restricted class abstraction. (Contributed by AV, 16-Jul-2019) (Revised by AV, 26-Mar-2021)

	Ref	Expression
Hypotheses	rabex2.1	|- B = { x e. A | ps }
	rabex2.2	|- A e. _V
Assertion	rabex2	|- B e. _V

Proof

Step	Hyp	Ref	Expression
1		rabex2.1	|- B = { x e. A | ps }
2		rabex2.2	|- A e. _V
3		id	|- ( A e. _V -> A e. _V )
4	1 3	rabexd	|- ( A e. _V -> B e. _V )
5	2 4	ax-mp	|- B e. _V