Theorem sepab

Description: Separation Scheme (Aussonderung) in terms of a class abstraction. (Contributed by NM, 8-Jun-1994) Put in closed form. (Revised by BJ, 18-Jul-2026)

	Ref	Expression
Assertion	sepab	⊢ ( 𝐴 ∈ 𝑉 → { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ∈ V )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑉 )
2		ssab2	⊢ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ⊆ 𝐴
3	2	a1i	⊢ ( 𝐴 ∈ 𝑉 → { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ⊆ 𝐴 )
4	1 3	ssexd	⊢ ( 𝐴 ∈ 𝑉 → { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ∈ V )