Class Member of Class Builder
Jump to navigation
Jump to search
Theorem
Let $A$ be a class.
Let $x$ be a set.
Let $P \left({x}\right)$ be a well-formed formula in the language of set theory.
Let $P \left({A}\right)$ denote the formula $P\left({x}\right)$ with all free instances of $x$ replaced with instances of $A$.
Let $\left\{{x: P \left({x}\right)}\right\}$ be a class specified using class builder notation.
Then:
- $A \in \left\{{x : P \left({x}\right)}\right\} \iff \left({\exists x: x = A \land P \left({A}\right)}\right)$
Proof
\(\ds A \in \left\{ {x : P \left({x}\right)}\right\}\) | \(\implies\) | \(\ds \exists x \in \left\{ {x : P \left({x}\right)}\right\}: A = x\) | Definition of class membership | |||||||||||
\(\ds \) | \(\implies\) | \(\ds \exists x: \left({x = A \land P \left({x}\right)}\right)\) | Definition of bounded existential quantifier | |||||||||||
\(\ds \) | \(\implies\) | \(\ds \exists x: \left({x = A \land P \left({A}\right)}\right)\) | Substitutivity of Class Equality |
$\blacksquare$
Also see
Sources
- 1971: Gaisi Takeuti and Wilson M. Zaring: Introduction to Axiomatic Set Theory: $\S 4.12$