Exercise 2, § 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.

Let $\mathscr{T}$ be an equalitarian theory, let $R$ be a relation in $\mathscr{T}$, and let $x$, $y$ be distinct letters; in particular $x$ is not a constant of $\mathscr{T}$. By the earlier exercise (ens-i-s5-ex-1) the relation $x = y$ is functional in $x$ in $\mathscr{T}$. We apply C47 of §5, no. 3 with $R\{x\}$ taken as $x = y$ and $S\{x\}$ taken as the given relation $R$. Since $x = y$ is functional in $x$, C47 asserts that the relation $S\{\tau_x(x = y)\}$ is equivalent to $(\exists x)((x = y) \text{ and } R)$.

Now we determine the term $\tau_x(x = y)$. Because $x = y$ is functional in $x$, C46 of §5, no. 3 gives $(x = y) \Leftrightarrow (x = \tau_x(x = y))$. Moreover, by Theorem 1 (tag 03P3) the relation $y = y$ is a theorem in $\mathscr{T}$; that is, $(y|x)(x = y)$ is true. Since $x = y$ is single-valued in $x$ (it is functional), C45 of §5, no. 3 yields $(y|x)(x = y) \Rightarrow (y = \tau_x(x = y))$. Hence $y = \tau_x(x = y)$ is a theorem. By Theorem 2 (tag 03P4), symmetry of equality gives $\tau_x(x = y) = y$ as a theorem.

Scheme S6 (substitution of equals) then implies $(\tau_x(x = y)|x)R \Leftrightarrow (y|x)R$, i.e. $S\{\tau_x(x = y)\}$ is equivalent to $(y|x)R$. By transitivity of equivalence, $(\exists x)(x = y \text{ and } R)$ is equivalent to $(y|x)R$ in $\mathscr{T}$.