The axiom of separation, derived as a theorem from the more general
axiom of class comprehension. More precisely, it represents an
axiom schema, namely an axiom for every predicate P which stands for
an arbitrary formula. It could be stated in existential form as
∃B. ∀u. u ∈ B ↔ u ∈ A ∧ P u,
but this set B is uniquely determined, as separation_is_unique
shows. Thus we may introduce
{x | x ∈ A ∧ P x} := B
by definitional extension.
Proof
01. 1 ⊢ u ∈ {x | x ∈ A ∧ P x}, hypo.
02. 1 ⊢ u ∈ A ∧ P u, comp_elim 1.
03. ⊢ u ∈ {x | x ∈ A ∧ P x} → u ∈ A ∧ P u, subj_intro 2.
04. 4 ⊢ u ∈ A ∧ P u, hypo.
05. 4 ⊢ u ∈ A, conj_eliml 4.
06. 4 ⊢ set u, set_intro 5.
07. 4 ⊢ u ∈ {x | x ∈ A ∧ P x}, comp_intro 6 4.
08. ⊢ u ∈ A ∧ P u → u ∈ {x | x ∈ A ∧ P x}, subj_intro 7.
separation. ⊢ u ∈ {x | x ∈ A ∧ P x} ↔ u ∈ A ∧ P u, bij_intro 3 8.
Dependencies
The given proof depends on one axiom:
comp.