Theorem comp_elim

Proof
01. ⊢ u ∈ {x | P x} ↔ set u ∧ P u, comp.
02. ⊢ u ∈ {x | P x} → set u ∧ P u, bij_eliml 1.
03. 3 ⊢ u ∈ {x | P x}, hypo.
04. 3 ⊢ set u ∧ P u, subj_elim 2 3.
05. 3 ⊢ P u, conj_elimr 4.
comp_elim. ⊢ u ∈ {x | P x} → P u, subj_intro 5.

Dependencies
The given proof depends on one axiom:
comp.