I'm currently reading through an introductory book to proofs and have just stumled upon the unique existential quantifier $\exists!$
On the book as well as on Wikipedia it says that $\exists!$ has the following equivalence:
$$(\exists! x) \equiv (\exists x)A(x) ∧ (\forall y)(\forall z)(A(y) ∧ A(z) \Rightarrow y = z)$$
My question is the following: doesn't this last expression allow for weird behaviour? For example, $A(y)$ could be True and $A(z)$ be False and still have $y = z$ be True, without making the conditional $(A(y) ∧ A(z) \Rightarrow y = z)$ False. Does this hold up simply because of the fact that you will never both have $A(y)$ be T, $A(z)$ be F and $y = z$ be T?
This should really be a comment, but it's too long.
You ask:
(I've switched to more standard notation for true/false.) Yes, you are correct, and this is due to the special logical properties of equality.
To unpack this, it may be helpful to consider a generalization of the unique existential quantifier. Suppose I have a binary relation symbol $E$ in my language; then the $E$-unique existential quantifier $\exists!_E$ is defined as follows:
$$\exists!_Ex\varphi(x)\quad\equiv\quad [\exists x\varphi(x)]\,\,\wedge\,\,[\forall x\forall y(\varphi(x)\wedge\varphi(y)\implies xEy)].$$
If you want to think about things graph-theoretically, this says that the set of $x$ satisfying $\varphi$ forms an "$E$-clique". We also have the strong $E$-unique existential quantifier $\exists!^+_E$ defined as follows:
$$\exists!_E^+x\varphi(x)\quad\equiv\quad [\exists x\varphi(x)]\,\,\wedge\,\,[\forall x\forall y(\varphi(x)\wedge\varphi(y)\implies xEy)]\,\,\wedge\,\,[\forall x\forall y(\varphi(x)\wedge xEy\implies \varphi(y))].$$
Note the additional clause. Graph-theoretically, this says that the set of $x$ satisfying $\varphi$ forms a maximal $E$-clique.
These quantifiers can be very oddly behaved. For example, whenever $\exists!_E$ and $\exists!_E^+$ aren't the same we have some $a, b$ and some formula $\varphi$ such that $\exists!_Ex\varphi(x)$ holds, $\varphi(a)$ and $aEb$ hold but $\varphi(b)$ fails; this is the situation you're worried about but with $=$ replaced with $E$. Indeed, this situation characterizes the phenomenon "$\exists!_E\not=\exists!_E^+$."
However, note that in the special case where we use $=$ for $E$ we gain the additional power of knowing how $=$ behaves. For example, $=$ satisfies the substitution property: $\varphi(x)$ and $x=y$ implies $\varphi(y)$. This immediately tells us that $\exists!_=$ and $\exists!_=^+$ are the same, and in particular the situation you're worried about can't happen.
The point is that by thinking about the "generalized" unique existential quantifiers, we see that your worry is avoided not because of anything fancy in the definition of the unique existential quantifier but rather the basic logical properties of equality.