How would you prove in FOL that x is a member of {x} for all x? How can I formulate and prove the following in first-order logic?
$$\forall x (x\in \{x\})$$
I have the following two statements:


*

*member(x,$\alpha$)

*$\neg \exists y(\text{member}(y,\alpha )\land x\neq y)$


The latter means, of course, that there does not exist another member of $\alpha$ distinct from $x$. That is, $x$ is the only member of $\alpha$.
However, while this seems to establish $\alpha$ as {$x$}, it does not seem to get me any closer to proving that every x is a member of the set containing only itself.
What am I doing wrong? Do I need to use axioms of set theory in this proof? I am familiar with the NBG (Von Neumann–Bernays–Gödel) axioms. Which axioms are needed, and how?

Along the lines suggested by Henning, we can let $U$ be domain of quantification. We can then think of  $\{x\}$ as an operator/function mapping $U$ to the $P(U)$. Such a function can be constructed using the power set, Cartesian product and subset rules of ordinary set theory such that $\forall a,b\in U: [a\in \{b\}\iff a=b]$. Then, of course, $\forall x\in U: x\in \{x\}$ as required.
