For any $x$ there exist a set $X$ such that $X=\{x\}$ Clearly for the Pair Axiom for any $x,y$ there esist a set $X$ such that $X=\{x,y\}$ and so for any $x$ there exist a set $X$ such that $X=\{x,x\}$. Unfortunately how prove that $\{x,x\}=\{x\}$? Indeed clearly if $\{x\}$ is a set the statement is trivially true, but unfortunately I don't know if $\{x\}$ is a set: anyway I'm sure that $x$ is the unique element of $X$! so could I formally conclude that $X=\{x\}$? I point out that I use ZFC axiomatization and I found this statement in "Introduction to Set Theory" by Karel Hrbacek and Thomas Jech where it is written that $\{x,x\}\pmb{:=}\{x\}$, but unfortunately I doubt about the strictness of this definition respect ZFC. So could someone help me? I know that the question could seem trivially; but if we have a carefully inspection then it seems insidious.
 A: What does $X = \{x\}$ mean? It means that (1) $x$ is an element of $X$, and every element of $X$ is equal to $x$. 
By the Pair axiom, there exists a set $\{x,x\}$. What does this mean? It means that (2) $x$ is an element of $X$, $x$ is an element of $X$, and every element of $X$ is equal to $x$ or equal to $x$. 
But (1) and (2) are equivalent, just by basic logic. 

Let me try to clarify what I wrote above. You want to prove that $\{x\} = \{x,x\}$. This is immediate from the axiom of extensionality. To prove that $X = Y$, we just need to prove that every element of $X = \{x\}$ is an element of $Y = \{x,x\}$ and vice versa. Well, let $a\in X$. Than $a = x$. So $a\in Y$. Conversely, let $a\in Y$. Then $a = x$ or $a = x$. In either case, $a\in X$. So we're done. 

Now for a more formal answer. The language of set theory, in which ZFC is axiomatized, does not contain the symbols $\{$ and $\}$. We use these symbols when we talk informally about set theory. When we write $\{a_1,\dots,a_n\}$, we mean a set which contains the elements $a_1,\dots,a_n$ and no others. 
In ZFC, we can express the informal statement $X = \{a_1,\dots,a_n\}$ with the following formula: $$\left(\bigwedge_{i=1}^n a_i\in X\right) \land \forall y\, \left(y\in x\rightarrow \bigvee_{i=1}^n y = a_i\right).$$ This says that each $a_i$ is an element of $X$, and every element of $X$ is equal to one of the $a_i$. 
So the formula defining $\{x\}$ (and corresponding to my condition (1) above) is $\varphi(X):$ $$x\in X\land \forall y\, (y\in X\rightarrow y = x).$$
And the formula defining $\{x,x\}$ (and corresponding to my condition (2) above) is $\psi(X)$: $$x\in X\land x\in X \land \forall y\, (y\in X\rightarrow (y = x\lor y = x)).$$
But these are logically equivalent formulas!  That is, $\forall X\, (\varphi(X)\leftrightarrow \psi(X))$. 
You ask whether we can prove that $\{x\} = \{x,x\}$. This means proving $\forall X\forall Y\, (\varphi(X)\land \psi(Y)\rightarrow X = Y)$. Yes, you can prove this in ZFC using the axiom of extensionality, as I explained above.  
A: This is just a simplification of Alex Kruckman's answer.
$\{ \}$ is a defined symbol, it is not a primitive of the language of ZFC, [if it was a primitive of the language, then your question stands correct!] and the definition of it is as:
$x=\{a_1,..,a_n\} \equiv_{df} \forall y (y \in x \leftrightarrow y=a_1 \lor ..\lor y=a_n)$
Now for the case of pairing we have ZFC having the axiom of pairing:
$\forall a \forall b \exists x \forall y (y \in x \leftrightarrow y=a \lor y=b)$
Now lets substitute $a$ instead of $b$, then we'll have:
$\forall a \exists x \forall y (y \in x \leftrightarrow y=a \lor y=a)$
So by definition of $\{\}$ we have: $\forall a \exists x (x=\{a,a\})$
But logically $y=a \lor y=a \leftrightarrow y=a$
So ZFC proves: 
$\forall a \exists x \forall y (y \in x \leftrightarrow y=a)$
and by definition of $\{\}$ this leads to ZFC proving:
$\forall a \exists x (x=\{a\})$.
And clearly by Extensionality $\{a\}=\{a,a\}$
A: A set can be defined in three ways
By extension $\{...\}$
$\{x\}$ is a set with single element.
By comprehension $\{x\in .. : ...\}$
By a Venn diagram.
on the other hand, an object of the set theory, can be seen as a set or an element.
$\{x,y\}$ is set.
$y$ is an element.
$y\cup \{\{y,x)\} $  is a set.
A: I presume your version of axiomatic set theory defines sets implicitly as the objects produced by applying the axioms.  So...


*

*The empty set, $\varnothing$, is a set by the empty set axiom.

*The powerset of $\varnothing$, which is $\{\varnothing\}$ establishes the existence of a one element set.

*For the $x$ in your $X = \{x,x\}$, construct the functional predicate $f_x$ by the relation $\{\varnothing \mapsto x\}$, then use the axiom of replacement to obtain $\{x\}$.


This establishes that $\{x\}$ is a set for any  $x$.
For the equality $\{x\} = \{x,x\}$, use the axiom of extensionality.  Every element of $\{x\}$ is an element of $\{x,x\}$ by an exhaustive check of one element.  Every element of $\{x,x\}$ is an element of $\{x\}$ by an exhaustive check of two elements.  Therefore, the equality holds.
