# Prove sequent using natural deduction

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$
• In short: Since you wish to use Universal (Re)Introduction twice, this is a clue to first use Universal Elimination twice. Commented Dec 28, 2017 at 4:54
• Short answer is, you want step 4 to be $P(x_0) \land P(z_0)$ Commented Dec 28, 2017 at 7:20

$$\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}$$