Is (∀)(∀) (¬ =  ∨  = ) → (∀)(¬ =  ∨  = ) an instance of (∀x)A → A[x:=t]? "(∀x)A → A[x:=t]"  means "If a statement A is true for all
x, then it must be true of any special value t that we are allowed to plug into x." 
 A: No, because the substitution in $A[x:=t]$ must avoid variable captures.
Different textbooks differ in exactly how they formalize this rule. (There are even some that just wave their hands apologetically and say not much more than I did here).
One fairly simple way to implement it is that you can't do
$$ \bigl[ \forall x(\cdots)\bigr] [y:=t] $$
if $x$ appears in $t$ without first renaming the dummy variable $x$ in the quantifier. In that case if you want to apply your rule to the case in the question title you would get
$$ \bigl[\forall x(x\ne y \lor x=y)\bigr][y:=x] \quad\equiv\quad
\forall z(z\ne x \lor z=x)$$
because we first rename the dummy variable $x$ to $z$ before we can substitute the term $x$ in. This would give you the instance
$$ \forall y \forall x (x\ne y \lor x=y) \to \forall z(z\ne x \lor z=x) $$
which is certainly true enough.
You could get $\forall x(x\ne x\lor x=x)$ from the conclusion of this by now instantiating $z$ to $x$, and then applying universal generalization to $x\ne x\lor x=x$.
The availability of this small detour can make it seem like the rule against variable capture is toothless in the first place, but it only works because the $\forall z$ (which was the original $\forall x$) is the top-level logical construction of the formula. If it was deeper in the structure of the formula -- say, beneath a bunch of $\to$ or $\neg$, then we couldn't just instantiate it and then re-generalize.
