The following is Rule D (Change of Variables) from Chapter 1, Section 3 of Paul Cohen's "Set Theory and the Continuum Hypothesis":
If $A$ is any statement and $A'$ results from $A$ by replacing each occurrence of the symbol $x$ with the symbol $x'$, where $x$ and $x'$ are any two variable symbols, then the statement $(A) \leftrightarrow (A')$ is a valid statement.
Should this rule have been qualified by some further requirement that limits the occurrences of $x$ in $A$? Or, as seems more likely, is there something I'm missing?
With the rule as stated, we can take the statement $A$ to be $\forall x \exists y\,(y>x)$. If we replace each occurrence of $y$ by $x$, does this not give rise to the (hopefully non-valid) sentence $(\forall x \exists y\,(y>x)) \leftrightarrow (\forall x \exists x\,(x>x))$? Or am I missing a technical aspect of the semantic interpretation of sentences with doubly-bound variables, which would make this statement trivially valid?
No, you are not missing something, and yes, you are right that this rule should have been qualified by saying that none of the $x$'s that are being replaced by $x'$'s may occur within the scope of an already existing quantifier for $x'$