Class Member of Class Builder
Jump to navigation
Jump to search
The validity of the material on this page is questionable.
Class Membership def can't be applied because, being in ZF, we can't quantify over classes. Use DefAbbrev on Definition:Class/Zermelo-Fraenkel instead
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by resolving the issues.
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$
Class Membership def can't be applied because, being in ZF, we can't quantify over classes. Use DefAbbrev on Definition:Class/Zermelo-Fraenkel instead
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by resolving the issues.
To discuss this proof in more detail, feel free to use the talk page.
If you are able to fix this page, then when you have done so you can remove this instance of {{Questionable}} from the code.
If you would welcome a second opinion as to whether your correction is correct, add a call to {{Proofread}} the page (see the proofread template for usage).
Also see
Sources
- 1971: Gaisi Takeuti and Wilson M. Zaring: Introduction to Axiomatic Set Theory: $\S 4.12$