Remark

Let $R$ be a relation which is collectivizing in $x$, and let $S$ be a relation such that $(\forall x)(S \Rightarrow R)$ is a theorem. Then $S$ is collectivizing in $x$; for $R$ is equivalent to $x \in \mathscr{E}_x(R)$, so that

is a theorem, and the assertion follows from C52. Notice also that in this case we have $\mathscr{E}_X(S) \subset \mathscr{E}_X(R)$ by C50.

C53. Let $T$ be a term, $A$ a set, $x$ and $y$ distinct letters. Suppose that $x$ does not appear in $A$ and that $y$ does not appear in $A$ nor in $T$. Then the relation $(\exists x)(y = T$ and $x \in A)$ is collectivizing in $y$.

Let $R$ be the relation $y = T$. The relation $(\forall y)(R \Rightarrow (y \in \{T\}))$ is true, hence so is $(\forall x)(\exists X)(\forall y)(R \Rightarrow (y \in X))$, where $X$ is a letter, distinct from $y$, which does not appear in $R$. By virtue of S8, the relation $(\exists x)(x \in A$ and R) is collectivizing in $y$, and C53 is proved.

¶ The relation $(\exists x)(y = T$ and $x \in A)$ is often read as follows : "$y$ can be put in the form $T$ for some $x$ belonging to $A$". The set

is generally called the set of objects of the form $T$ for $x \in A$. The assembly so denoted contains neither $x$ nor $y$, and does not depend on the choice of the letter $y$ satisfying the conditions of C53.