Prove sequent using natural deduction

Question

I need to prove the following predicate logic sequent using natural deduction:

$\exists y \forall x (P(x) \rightarrow x = y) \vdash \forall x \forall y (P(x) \land P(y) \rightarrow x = y)$

This is my half-finished proof. I hope I'm on the right track but there is something about box packing/unpacking I don't understand yet:

1. $\exists y \forall x (P(x) \rightarrow x = y) \quad\mathrm{Premise}$
2. $y_0: \forall x P(x) \rightarrow x = y_0) \quad\mathrm{Assumption}$
3. $x_0: P(x_0) \rightarrow x_0 = y_0 \quad \forall x e2$
4. $P(x_0) \land P(y_0) \quad \mathrm{Assumption}$
5. $P(x_0) \quad \land e_1 4$
6. $x_0 = y_0 \quad \rightarrow e 3, 5$
7. $P(x_0) \land P(y_0) \rightarrow x_0 = y_0 \quad \rightarrow i 4-6$
8. $\forall x (P(x) \land P(y_0) \rightarrow x = y_0 \quad \forall x i 3-7$

Then I can't go further because I can't use universal reintroduction on the $y$ variable.

Edit: I managed to finish it with the help from the answer!

1. $\exists y \forall x (P(x) \rightarrow x = y) \quad\mathrm{Premise}$
2. $z: \forall x P(x) \rightarrow x = z) \quad\mathrm{Assumption}$
3. $a: P(a) \rightarrow a = z \quad \forall x e2$
4. $b: P(b) \rightarrow b = z \quad \forall x e2$
5. $P(a) \land P(b) \quad \mathrm{Assumption}$
6. $P(a)\quad \land e_1 5$
7. $P(b)\quad \land e_2 5$
8. $a = z \quad \rightarrow e3,6$
9. $b = z \quad \rightarrow e4,7$
10. $b = b \quad =i$
11. $z = b \quad =e 9,10$
12. $a = b \quad =e 8,11$
13. $P(a) \land P(b) \rightarrow a = b \quad \rightarrow i 5-12$
14. $\forall y (P(a) \land P(y) \rightarrow a = y) \quad \forall y i 4-13$
15. $\forall x \forall y (P(x) \land P(y) \rightarrow x = y) \quad \forall x i 3-14$
16. $\forall x \forall y (P(x) \land P(y) \rightarrow x = y) \quad \exists z e 1,2-15$

Answer 1

You almost have it.   Do pretty much as you had, except use universal elimination twice, then conclude that the two arbitrary variables must be equal whenever they both make the predicate true, since they would both then equal the same witness.

$$\begin{array}{r|l:l}1&\exists y\forall x~(P(x)\to x=y)\\ 2&\quad\forall x~(P(x)\to x=c) & 1,\exists \text{Elimination }[y\backslash c]\\[0ex] 3 & \qquad P(a)\to a=c & 2,\forall\text{Elimination }[x\backslash a]\\[0ex] 4 & \qquad\quad P(b)\to b=c & 2,\forall\text{Elimination }[x\backslash b] \\[0ex] 5 & \qquad\qquad P(a)\wedge P(b) & \text{Assumption} \\[-1ex] 6 & \qquad\qquad\vdots & \\[-1ex] 7 & \qquad\qquad\vdots & \\[-1ex] 8 &\qquad\qquad\vdots & \\[-1ex] 9 & \qquad\qquad\vdots & \\[0ex] 10 & \qquad\qquad a=b & ~,~,=\text{Elimination}\\[0ex] 11 & \qquad\quad (P(a)\wedge P(b))\to(a=b) & 5,10,\to\text{Introduction}\\[-1ex] \vdots\end{array}$$

Well, you can fill in the missing details.