Theorem zfausab

Description: Separation Scheme (Aussonderung) in terms of a class abstraction. (Contributed by NM, 8-Jun-1994)

	Ref	Expression
Hypothesis	zfausab.1	⊢ 𝐴 ∈ V
Assertion	zfausab	⊢ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ∈ V

Proof

Step	Hyp	Ref	Expression
1		zfausab.1	⊢ 𝐴 ∈ V
2		ssab2	⊢ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ⊆ 𝐴
3	1 2	ssexi	⊢ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ∈ V