Specification Axiom Schema

The Specification Axiom, technically an axiom schema, is a possible axiom schema of Material set theory: #m/def/set/zf Let $𝜑 (𝑥)$ be a Predicative formula (i.e. unary definite condition) of set theory. Then,

(\forall 𝔐 𝐴) (\exists 𝔐 𝐵) [𝑥 \in 𝐵 ⟺ 𝑥 \in 𝐴 \land 𝜑 (𝑥)]

which is to say, there exists a subset $𝐵$ of $𝐴$ containing all those elements $𝑥$ of $𝐴$ for which $𝜑 (𝑥)$ . By the Axiom of Extensionality such a set is unique, and we denote it using Set builder notation as

𝐵 = {𝑥 \in 𝐴 : 𝜑 (𝑥)}

#state/tidy | #lang/en | #SemBr