All instances of x are bound and no instances of y are bound.

In many contexts, we often leave off the universal quantifiers. If you wish to know whether an instance of a variable is bound or not in a formula, then just specify whether you mean the formula as it is actually displayed or as it is, in some context, understood to stand for the universal closure of the displayed formula.

If "for all x, x-y=x+(-y)" is to be regarded as actually displayed, then no instances of y are bound in it.

If "for all x, x-y=x+(-y)" is to be regarded as standing for its universal closure "for all y, for all x, x-y=x+(-y)" then all instances of y are bound in it.

Note that the key theorem of logic for this matter is:

For all formulas F we have |- F if and only if |- AxF. But it is not the case that for all formulas F we have |- F <-> AxF.