Problem with the compact version of the definition for "exactly one" According to the definition, if we want to express that there is exactly one $x$ such that $P(x)$, we specify:
$\exists x (P(x) \wedge \forall y (P(y) \rightarrow y = x))$
By Existential Instantiation we can say that $P(a) \wedge \forall y (P(y) \rightarrow y = a)$.
Since we are not dealing with a biconditional, but just a conditional, we cannot infer the following from just the previous statement:
$\forall y (y = a \rightarrow P(y))$
Which is counter intuitive, for we would expect that any $y$ satisfying $P$ would precisely be $a$.
However, we find that there is a more compact definition of exactly one by stating it like this:
$\exists x \forall y (P(x) \leftrightarrow y = x)$
Once again, by Existential Instantiation we can write:
$\forall y (P(y) \leftrightarrow y = a)$
This time implying that $\forall y (y = a \rightarrow P(y))$.
Then... what just happened?
 A: 
By Existential Instantiation we can say that $P(a) \wedge \forall y (P(y) \rightarrow y = a)$.
Since we are not dealing with a biconditional, but just a conditional, we cannot infer the following from just the previous statement:
$\forall y (y = a \rightarrow P(y))$

No, of course we can infer that.  We are not dealing with just a conditional, but rather with a conjunction and a conditional.   Since $P(a)$ therefore $\forall y~(y{=}a\to P(y))$, and hence$$P(a)\wedge \forall y~(P(y)\to y=a)\dashv\vdash \forall y~\Big(\big(y=a\to P(y)\big)~\wedge~\big(y\neq a\to\neg P(y)\big)\Big)$$
A: For the first definition, with the equality axiom for formulas we can easily derive:

$P(x) \vdash y=x \to P(y)$.

In details:
1) $∃x \ (P(x) ∧ ∀y(P(y) → y=x))$ --- premise
2) $P(a) ∧ ∀y(P(y) → y=a)$ --- from 1) by Existential Instantiation (I would prefer to use $\exists$-Elim...)
3) $∀y(P(y) → y=a)$ --- from 2) by Conjunction Elimination
4) $P(y) → y=a$ --- from 3) by Universal Instantiation
5) $P(a)$ --- from 2) by Conjunction Elimination
6) $y=a$ --- assumed [*]
7) $\vdash y=a \to a=y$ --- symmetry: provable from equality axioms
8) $a=y$ --- from 6) and 7) by Modus Ponens ($\to$-Elimination)
9) $\vdash a=y \to (P(a) \to P(y))$ --- equality axiom
10) $P(a) \to P(y)$ --- from 8) and 9) by Modus Ponens
11) $P(y)$ --- from 5) and 10) by Modus Ponens
12) $y=a \to P(y)$ --- from 6) and 11) by Conditional Proof (or $\to$-Introduction), discharging assumption [*]

13) $P(y) \leftrightarrow y=a$ --- from 4) and 12) by $\leftrightarrow$-Introduction

14) $\forall y \ (P(y) \leftrightarrow y=a)$ --- from 13) by Generalization ($\forall$-Introduction)


15) $\exists x \ \forall y \ (P(y) \leftrightarrow y=x)$ --- from 14) by $\exists$-Introduction.


In conclusion, we have:

$∃x \ (P(x) ∧ ∀y(P(y) → y=x)) \vdash \exists x \ \forall y \ (P(y) \leftrightarrow y=x)$.

In a similar way we can prove the equivalence of the two definitions.
A: That's right that you cannot turn an implication without other justification. However there is justification here as we have also $P(a)$ in the statement. It's by the axiom of equality you have $y=a\rightarrow P(y)$ due to $P(a)$.
A: 
$P(a) \wedge \forall y (P(y) \rightarrow y = a)$.
Since we are not dealing with a biconditional, but just a conditional, we cannot infer the following from just the previous statement:
$\forall y (y = a \rightarrow P(y))$

Sure we can!  Given that $a$ has property $P$, anything that is identical to $a$ will have to have property $P$ as well.
In other words, $\forall y (y = a \rightarrow P(y))$ logically follows from $P(a)$, and therefore also from $P(a) \wedge \forall y (P(y) \rightarrow y = a)$.
I am guessing that you thought it didn't, because you were too focused on the second conjunct.
