Class Member of Class Builder
Jump to navigation
Jump to search
Theorem
Let $A$ be a class.
Let $x$ be a set.
Let $\map P x$ be a well-formed formula in the language of set theory.
Let $\map P A$ denote the formula $\map P x$ with all free instances of $x$ replaced with instances of $A$.
Let $\set {x: \map P x}$ be a class specified using class builder notation.
Then:
- $A \in \set {x: \map P x} \iff \paren {\exists x: x = A \land \map P A}$
Proof
\(\ds A\) | \(\in\) | \(\, \ds \leftset x \, \) | \(\, \ds : \, \) | \(\ds \rightset {\map P x}\) | ||||||||||
\(\ds \leadsto \ \ \) | \(\ds \exists x \in \set {x: \map P x}: \, \) | \(\ds A\) | \(=\) | \(\, \ds x \, \) | \(\ds \) | Definition of Class (Zermelo-Fraenkel) | ||||||||
\(\ds \leadsto \ \ \) | \(\ds \exists x: \, \) | \(\ds x\) | \(=\) | \(\, \ds A \, \) | \(\, \ds \land \, \) | \(\ds \map P x\) | Definition of Bounded Existential Quantifier | |||||||
\(\ds \leadsto \ \ \) | \(\ds \exists x: \, \) | \(\ds x\) | \(=\) | \(\, \ds A \, \) | \(\, \ds \land \, \) | \(\ds \map P A\) | Substitutivity of Class Equality |
$\blacksquare$
Also see
Sources
- 1971: Gaisi Takeuti and Wilson M. Zaring: Introduction to Axiomatic Set Theory: $\S 4.12$