ThmDex – An index of mathematical definitions, results, and conjectures.
P2774
Set $Y : = \{ \{ x \} : x \in X \}$. If $X$ is empty, then $Y$ is also empty and the claim is a consequence of R2766: Canonical empty map is bijection.

Suppose thus that $X$ is nonempty and let $x, y \in X$ be such that $f(x) = f(y)$. Then $\{ x \} = f(x) = f(y) = \{ y \}$, whence $x = y$, so that $f$ is injective.

If $y \in Y$, then $y = \{ x \}$ for some $x \in X$ such that $f(x) = \{ x \} = y$, so $f$ is also surjective. Since $f$ is both an injection and a surjection, that $f$ is a bijection then follows from R1478: Equivalent characterisations of bijectivity. $\square$