The complex conjugate $\overline{z}$ is defined as $\overline{z} = (x, - y)$. If $y = 0$, then result
R4483: Real number is zero iff equal to its reflection shows that $y = - y$ and we have
\begin{equation}
\overline{z}
= (x, - y)
= (x, y)
= z
\end{equation}
Conversely, assume that $\overline{z} = z$ holds. Then
\begin{equation}
(x, - y)
= \overline{z}
= z
= (x, y)
\end{equation}
whence result
R3346: Characterisation of equality of ordered pairs states that $x = x$ and, in particular, $- y = y$. Result
R4483: Real number is zero iff equal to its reflection now shows that $y = 0$. $\square$
