Determine under which conditions the formula $\phi[t/x]\leftrightarrow \forall x ((x=t)\rightarrow \phi)$ is logically true I am stucked at this problem for a long time:

Determine under which conditions the following first-order formula is logically true
$$\phi[t/x]\leftrightarrow \forall x ((x=t)\rightarrow \phi)$$
where $t$ is a term, $x$ is a variable, $\phi$ is a formula and $\phi[t/x]$ denotes that we are substituting the term $t$ in place of the free occurrences of the variable $x$ in the string $\phi$ and that none of the variables in $t$ becomes bound to one of the quantifieres in $\phi$ (If any).


For the $\rightarrow$ side we can deduce as follows: let $K=\{\phi[t/x]\}$, now (1) $K\vdash \phi[t/x]$ (2) $K\vdash \phi[t/x]\rightarrow ((t=t)\rightarrow \phi[t/x])$ (3) $K\vdash ((t=t)\rightarrow \phi[t/x])$ , Now I do not know how to conclude $K\vdash \forall x((x=t)\rightarrow \phi)$ ? Which axioms should I use?
Thanks for any hint/help.
 A: Ref to :


*

*Herbert Enderton, A Mathematical Introduction to Logic (2nd ed - 2001), Ex.13, page 130.


For $\leftarrow$ :
1) $∀x((x=t) \to \varphi)$ --- assumed
2) $(t=t) \to \varphi[t/x]$ --- from 1) and Enderton's Ax.2 : $∀xα \to α_t^x$, where $t$ is substitutable for $x$ in $\alpha$, and modus ponens
3) $\vdash t=t$ --- from equality axiom Ax.5
4) $\varphi[t/x]$ --- from 2) and 3) by mp

$\vdash ∀x((x=t) \to \varphi) \to \varphi[t/x]$ --- from 1) and 4) by Deduction Th.


For $\rightarrow$ :
We need the following :

Equality Theorem [see Shoenfield, page 35]. Let the term $b'$ be obtained from the term $b$ by replacing some occurrences of $a_1, \ldots ,a_n$ by $a_1', \ldots, a_n'$ respectively, and let the formula $A'$ be obtained from the formula $A$ by the same type of replacements.
If $\vdash a_1 = a_1', \ldots, \vdash a_n = a_n'$, then $\vdash b = b'$ and $\vdash A \leftrightarrow A'$.

It is provable by induction on the lenght of $b$. We have also [page 36] the 

Corollary 2. $\vdash a_1 = a_1' \to \ldots \to a_n = a_n' \to (A[a_1,\ldots, a_n] \leftrightarrow A[a_1',\ldots, a_n'])$. 

[It is the "generalization" of Enderton's equality axiom Ax.6 : $x = y \to (α → α')$, where $α$ is atomic and $α'$ is obtained from $α$ by replacing $x$ in zero or more (but not necessarily all) places by $y$.]
1) $\varphi[t/x]$ --- assumed : $x$ does not occur in $t$ and $t$ has replaced all the free occurrences of the variable $x$ in $\varphi$
2) $\vdash x=t \to (\varphi \leftrightarrow \varphi[t/x])$ --- from Coroll.2 above : $\varphi$ is $\varphi[x/x]$
3) $\vdash \varphi[t/x] \to (x=t \to \varphi)$ --- from 2) by tautological implication [Enderton's Lemma 24C (Rule T), page 118]
4) $(x=t \to \varphi)$ --- from 1) and 3) by mp
5) $\forall x (x=t \to \varphi)$ --- from 5) by Generalization Th : $x$ not free in 1), that means : $t$ must replace all free occurrences of $x$ in $\varphi$, and that $t$ has no occurrences of $x$

$\vdash \varphi[t/x] \to \forall x (x=t \to \varphi)$ --- from 1) and 5) by Deduction Th.

