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	⊢ 𝐵 = { 𝑦 ∈ 𝐴 ∣ 𝜓 }
	rab2ex.2	⊢ 𝐴 ∈ V
Assertion	rab2ex	⊢ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ∈ V

Proof

Step	Hyp	Ref	Expression
1		rab2ex.1	⊢ 𝐵 = { 𝑦 ∈ 𝐴 ∣ 𝜓 }
2		rab2ex.2	⊢ 𝐴 ∈ V
3	1 2	rabex2	⊢ 𝐵 ∈ V
4	3	rabex	⊢ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ∈ V