Theorem. comp_intro_from
u ∈ A → P u → u ∈ {x | P x}
Proof
01. 1 ⊢ u ∈ A, hypo.
02. 2 ⊢ P u, hypo.
03. 1 ⊢ set u, set_intro 1.
04. 1, 2 ⊢ u ∈ {x | P x}, comp_intro 3 2.
comp_intro_from. ⊢ u ∈ A → P u → u ∈ {x | P x}, subj_intro_ii 4.
Dependencies The given proof depends on one axiom: comp.