Proof of $x = y \leftrightarrow x \in \{y\}$

Question

Considering x and y are variables, to prove $x \in \{y\} \rightarrow x = y$, we have to assume the uniqueness of the element in $\{y\}$, which means $\forall z[z \in \{y\} \rightarrow z = y]$, and then apply universal instantiation. But I can't relate existence (if it is the case) to the proof of $x = y \rightarrow x \in \{y\}$.

Answer 1

Consider $\mathsf {ZFC}$; using Pairing axiom we prove that, for every $x,y$, the set $\{ x,y \}$ exists.

From this, with $x=y$, we have that also $\{ y \}$ exists and that $y \in \{ y \}$

Now, we have to use first-order substitution axioms for equality:

$y=x \to (y \in \{ y \} \to x \in \{ y \})$.

For the other part, by Pairing we have that $y$ is the unique element of $\{ y \}$. Thus, if $x \in \{ y \}$, then $x=y$.