comp_intro

Theorem comp_intro

Theorem. comp_intro
set u → P u → u ∈ {x | P x}

Proof
01. ⊢ u ∈ {x | P x} ↔ set u ∧ P u, comp.
02. ⊢ set u ∧ P u → u ∈ {x | P x}, bij_elimr 1.
03. 3 ⊢ set u, hypo.
04. 4 ⊢ P u, hypo.
05. 3, 4 ⊢ set u ∧ P u, hypo.
06. 3, 4 ⊢ u ∈ {x | P x}, subj_elim 2 5.
comp_intro. ⊢ set u → P u → u ∈ {x | P x}, subj_intro_ii 6.

Dependencies
The given proof depends on one axiom:
comp.