Class Member of Class Builder

From ProofWiki
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

\(\displaystyle A \in \left\{ {x : P \left({x}\right)}\right\}\) \(\implies\) \(\displaystyle \exists x \in \left\{ {x : P \left({x}\right)}\right\}: A = x\) Definition of class membership
\(\displaystyle \) \(\implies\) \(\displaystyle \exists x: \left({x = A \land P \left({x}\right)}\right)\) Definition of bounded existential quantifier
\(\displaystyle \) \(\implies\) \(\displaystyle \exists x: \left({x = A \land P \left({A}\right)}\right)\) Substitutivity of Class Equality

$\blacksquare$

Also see


Sources