 Free for substitution

A first-order term $\tau$ is free for substitution for a variable $z$ in a first-order formula when no free variable of $\tau$ becomes bound after replacing a free occurrence of $z$. Equivalently, at every free occurrence to be replaced, none of its enclosing quantifiers binds a variable appearing in $\tau$. The test depends on occurrences and scopes, not merely on which variable names appear anywhere in the formula.