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=\left\{y\in A|\psi \right\}$$
	rab2ex.2	$$⊢A\in \mathrm{V}$$
Assertion	rab2ex	$$⊢\left\{x\in B|\phi \right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		rab2ex.1	$$⊢B=\left\{y\in A|\psi \right\}$$
2		rab2ex.2	$$⊢A\in \mathrm{V}$$
3	1 2	rabex2	$$⊢B\in \mathrm{V}$$
4	3	rabex	$$⊢\left\{x\in B|\phi \right\}\in \mathrm{V}$$