Theorem sep_is_set

Theorem. sep_is_set
set A → set {x | x ∈ A ∧ P x}
Proof
01. 1 ⊢ set A, hypo.
02. ⊢ {x | x ∈ A ∧ P x} ⊆ A, sep_is_subclass.
03. 1 ⊢ set {x | x ∈ A ∧ P x}, subset 2 1.
sep_is_set. ⊢ set A → set {x | x ∈ A ∧ P x}, subj_intro 3.

Dependencies
The given proof depends on two axioms:
comp, subset.