Proof Using Natural Deduction (including '=' rules) I have a natural deduction proof that I'm stuck on. Obviously I'm not asking someone to just tell me the answer, but if anyone could help me with the next step/point out any mistakes I've made it would be much appreciated.
The proof is:
$P(b),\forall x\forall y(P(x)\wedge P(y) \rightarrow x=y) \vdash \forall x(P(x) \rightarrow x=b)$
and here is what I have so far:
$$1\;\;\;\;\;\;\;\;\;\;\;\;\; P(b)\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;  premise
\\ \;\;2\;\;\;\;\;\;\;\;\;\;\;\;\; \forall x \forall y(P(x)\wedge P(y) \rightarrow x=y) \;\;\;\;\;\;\;\;\;\;\;\;\;premise
\\ 3\;|\;x_0\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;
\\ \;\;\;\;\;4\;|\;|\;\;\;\;\;\;\;\;\;P(x_0)\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;assumption
\\ 5\;|\;|\;\;\;\;\;\;\;\;\; \forall y(P(x_0)\wedge P(y)\rightarrow x_0 = y)\;\;\;\;\;\;\;\;\;\;\;\;\;\forall e\;2\;\;\;\;
\\ 6\;|\;|\;\;\;\;\;\;\;\;\; P(x_0)\wedge P(y_0) \rightarrow x_0 = y_0\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\forall e\;5\;\;\;\;
\\ 7\;|\;|\;\;\;\;\;\;\;\;\;... \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;$$
I think from this point, I need to somehow show that $y_0 = b$ or $P(y_0)=P(b)$ or something, so that I can eliminate the $\rightarrow$ on line 6 and end up with $x_0=b$.
 A: You don't actually need to apply the identity rules. Note that in your givens you have $P(b)$ and $∀x∀y(P(x)∧P(y)→x=y)$, a sentence that merely asserts that one and only one object has $P$.
Now since $P$ is predicated of $b$ already, why don't try some instantiation of them?
You can try something simpler:

  
*
  
*$P(b)$, $\;\;\;\;\;\; \text{premise}$
  
*$∀x∀y(P(x)∧P(y)→x=y)$, $\;\;\;\;\;\; \text{premise}$

  
*$P(x)$, $\;\;\;\;\;\; \text{assumption}$
  
*$∀y(P(x)\land P(y)→x=y)$, $\;\;\;\;\;\; \text{2, $\forall$I}$
  
*$P(x)\land P(b)→x=b$, $\;\;\;\;\;\; \text{4, $\forall$I}$
  
*$P(x)\land P(b)$, $\;\;\;\;\;\; \text{3, 1, $\land$I}$
  
*$x=b$, $\;\;\;\;\;\; \text{5, 6, $\rightarrow$E}$
  
  
  
  $\;$ 8. $P(x) \rightarrow x=b$, $\;\;\;\;\;\; \text{2-7, $\rightarrow$I}$
$\;$ 9. $\forall x (P(x) \rightarrow x=b)$, $\;\;\;\;\;\; \text{2-7, $\rightarrow$I}$

A: I wouldn't bother instantiating $x_0$ or $y_0$. I would instantiate the $y$ in your second premise to be $b$ itself. Then since you have $P(b)$ as a premise, you know that $P(x) \land P(b)$ is equivalent to just $P(x)$, and you're done.
More explicitly, start with
$$\forall x\forall y(P(x)\wedge P(y) \rightarrow x=y$$
Then since this is true for every $y$, it must be true for $b$ in particular, so
$$\forall x(P(x)\wedge P(b) \rightarrow x=b$$
And since $P(b)$ is true, $P(x)\wedge P(b) \iff P(x)\wedge \top \iff P(x)$, so we can substitute and get
$$\forall x(P(x) \rightarrow x=b)$$
and done.
A: The 'trick' to remember is that when using universal elimination you can alpha-replace the bound entity with any entity, including a non-arbitrary entity.   If a predicate is true for all things it is true for any specific thing.   Just remember you can't use universal reintroduction when you don't choose an arbitrary entity.
You can use: $\forall y\; Q(y) \vdash Q(b)$ 
$$\def\fitch#1#2{~~\begin{array}{|l} #1\\\hline #2\end{array}}\fitch{~1.~P(b):\textsf{Premise (Constant Term)}\\~2.~\forall x\forall y~(P(x)\land P(y)\to x=y):\textsf{Premise}}{\fitch{~3.~[a]:\textsf{Arbitrary Term}}{~4.~\forall y~(P(a)\land P(y)\to a=y):\textsf{Universal Elimination (2,x:=a)}\\~5.~P(a)\land P(b)\to a=b:\textsf{Universal Elimination (4,y:=b)}\\\fitch{~6.~P(a):\textsf{Assumption}}{~7.~P(a)\land P(b):\textsf{Conjunction Introduction (1,6)}\\~8.~a=b:\textsf{Conditional Elimination (5,7)}}\\~9.~P(a)\to a=b:\textsf{Conditional Introduction (6-8)}}\\10.~\forall x~(P(x)\to x=b):\textsf{Universal Introduction (3-9)}}$$
