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?