I was trying the following exercise of identity of VanDalen's Predicate Logic. It is as follows.
$$\vDash \phi(t) \leftrightarrow \forall x(x=t \rightarrow \phi(x)), \ \ \ x \not \in FV(t)$$
It has a similar part of the Instant Axiom: $$ \vDash \forall x_1,\cdots,x_n, y_1,\cdots,y_n\ \wedge_{i\leq n} (x_i = y_i)\rightarrow (\phi(x_1,\cdots, x_n)\rightarrow \phi(y_1, \cdots, y_n)) $$
I was trying proving this exercise, going from $\forall x(x=t \rightarrow \phi(x))$ to $\phi(t)$. Using the axiom, we have
\begin{align*} &\vDash \forall x,t (x=t \rightarrow (\phi(x)\rightarrow\phi(t))\\ \text{and by introduction of }\wedge, \\ &\vDash \forall x,t (x=t \rightarrow (\phi(x)\rightarrow\phi(t))) \wedge \forall x(x=t \rightarrow \phi(x))\\ \text{because }x\not \in FV(t), \\ &\vDash \forall x,t (x=t \rightarrow (\phi(x)\rightarrow\phi(t)) \wedge (x=t \rightarrow \phi(x))\\ &\vDash \forall x,t (x=t \rightarrow (\phi(x)\rightarrow\phi(t)) \wedge \phi(x))\\ &\vDash \forall x,t (x=t \rightarrow \phi(t))\\ \end{align*}
I'm having problems finishing the entire proof, above is my unfinished version of rl-direction ($\Leftarrow$).
How do you prove it with a short or more clear way. Thanks.
Just apply the universally quantified statement to $t$, and you'll get "$t=t \to φ(t)$" after which you can get rid of the condition since it is true by an axiom. In general, don't pattern-match to guess which axioms to use (it won't work), but rather figure out what the statements themselves mean and how to construct or deconstruct them as appropriate. In this case where you want to prove the backward implication, you want to construct "$φ(t)$", and the only way you can do that using the given universal statement is to deconstruct it, and clearly applying it to $t$ is necessary to get what you want at all.