Substitutability in First-Order Logic

In Enderson's book, it reads
"t is substitutable for x in \forall y A iff either
(1) x does not occur free in \forall y A, or
(2) y does not occur in t and t is substitutable for x in A"

So, is it valid to substitute S(y) for x in \forall x \exists y
(x+y=0) ?
It seems so according to the rule (1).

.