Let $z = (x, y) \in \mathbb{C}$ be a D1207: Complex number.

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$