Exercise 1, § 5

This solution was written by nemotron-3-ultra-free and judged by a machine. It is not Bourbaki's and it has not been checked by a person.

The relation $x = y$ is functional in $x$ in $\mathscr{T}$ means that the relation “there exists exactly one $x$ such that $x = y$” is a theorem in $\mathscr{T}$. By definition this requires that $(\exists x)(x = y)$ is a theorem and that the relation “there exists at most one $x$ such that $x = y$” is a theorem in $\mathscr{T}$.

First we prove $(\exists x)(x = y)$. By Theorem 1 (03P3), $y = y$ is a theorem in $\mathscr{T}$. The assembly $(y|x)(x = y)$ is identical to $y = y$. By C33 (§4, no. 3), from $(y|x)(x = y)$ we deduce $(\exists x)(x = y)$. Hence $(\exists x)(x = y)$ is a theorem in $\mathscr{T}$.

Next we prove that “there exists at most one $x$ such that $x = y$” is a theorem. According to the criterion in §5, no. 3, it is enough to prove $u = v$ in the theory obtained by adjoining the hypotheses $(u|x)(x = y)$ and $(v|x)(x = y)$, where $u$ and $v$ are distinct letters distinct from $x$ and $y$ and not appearing in the explicit axioms of $\mathscr{T}$. These hypotheses are $u = y$ and $v = y$. By Theorem 2 (03P4), $v = y$ implies $y = v$. Then by Theorem 3 (03P5), from $u = y$ and $y = v$ we deduce $u = v$. Therefore $u = v$ is true under the adjoined hypotheses, so $x = y$ is single-valued in $x$ in $\mathscr{T}$, i.e., the relation “there exists at most one $x$ such that $x = y$” is a theorem in $\mathscr{T}$.

Since both conditions hold, the relation $x = y$ is functional in $x$ in $\mathscr{T}$.