Proof
01. 1 ⊢ u ∈ {x | x ∈ A ∧ P x}, hypo.
02. 1 ⊢ u ∈ A ∧ P u, comp_elim 1.
03. 1 ⊢ u ∈ A, conj_eliml 2.
04. ⊢ u ∈ {x | x ∈ A ∧ P x} → u ∈ A, subj_intro 3.
05. ⊢ ∀u. u ∈ {x | x ∈ A ∧ P x} → u ∈ A, uq_intro 4.
sep_is_subclass. ⊢ {x | x ∈ A ∧ P x} ⊆ A, incl_intro 5.
Dependencies
The given proof depends on one axiom:
comp.