Michael's point is that in a formal system there must be formal rules for manipulating symbols. So your provided textbook definition is not formal. In other words, we can say that there is simply a rule that allows us to rewrite either side of your equivalence into the other, and nothing to be proven. Note also that your second "$A(x)$" is redundant, and I'll ignore it for the rest of my answer (you can easily see how to include it after you've understood my answer).
But if you are not talking about a formal proof, but a model-theoretic proof, then you are no longer asking for a formal derivation, namely a sequence of statements allowed by the formal rules. Instead you would be asking for a proof outside the formal language that shows that given any model satisfying one side, it also satisfies the other. This we can 'do' as follows:
Given any model satisfying $\exists! x ( A(x) )$, let $x$ be a unique object such that $A(x)$ is true. Then $A(x)$ is true. Also, given any $y$, if $A(y)$ is true, then $y$ must be the same as $x$ because $x$ was unique. Thus $\forall y ( A(y) \rightarrow x = y )$ is true. Therefore $\exists x ( A(x) \land \forall y ( A(y) \rightarrow x = y )$ is true.
Similarly you can check that given any model satisfying $\exists x ( A(x) \land \forall y ( A(y) \rightarrow x = y )$ there will be a unique object $x$ such that $A(x)$ is true. Basically it exists because the given condition already guarantees existence. Also, it must be unique because any object satisfying $A$ is equal to it.
If you found this argument not satisfying, as if it is circular reasoning, it is indeed circular, because in our reasoning about models we are already using intuition corresponding to the equivalence we are purporting to prove! That is why some things must be accepted as either axioms that cannot be proven, or as definitions such as in this case. We simply define uniqueness according to the formal statement.
