Theorem rabexd

Description: Separation Scheme in terms of a restricted class abstraction, deduction form of rabex2 . (Contributed by AV, 16-Jul-2019)

	Ref	Expression
Hypotheses	rabexd.1	⊢ 𝐵 = { 𝑥 ∈ 𝐴 ∣ 𝜓 }
	rabexd.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
Assertion	rabexd	⊢ ( 𝜑 → 𝐵 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		rabexd.1	⊢ 𝐵 = { 𝑥 ∈ 𝐴 ∣ 𝜓 }
2		rabexd.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		rabexg	⊢ ( 𝐴 ∈ 𝑉 → { 𝑥 ∈ 𝐴 ∣ 𝜓 } ∈ V )
4	2 3	syl	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝜓 } ∈ V )
5	1 4	eqeltrid	⊢ ( 𝜑 → 𝐵 ∈ V )