Theorem rab2ex

Description: A class abstraction based on a class abstraction based on a set is a set. (Contributed by AV, 16-Jul-2019) (Revised by AV, 26-Mar-2021)

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

Proof

Step	Hyp	Ref	Expression
1		rab2ex.1	|- B = { y e. A | ps }
2		rab2ex.2	|- A e. _V
3	1 2	rabex2	|- B e. _V
4	3	rabex	|- { x e. B | ph } e. _V