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

Proof

Step	Hyp	Ref	Expression
1		rabex2.1	⊢ 𝐵 = { 𝑥 ∈ 𝐴 ∣ 𝜓 }
2		rabex2.2	⊢ 𝐴 ∈ V
3		id	⊢ ( 𝐴 ∈ V → 𝐴 ∈ V )
4	1 3	rabexd	⊢ ( 𝐴 ∈ V → 𝐵 ∈ V )
5	2 4	ax-mp	⊢ 𝐵 ∈ V