The notion of *alphabetical variant* is well known, so that a formula $x=x$ is an alphabetical variant of $y=y$ if $x$ and $y$ are distinct variables.

One may want to consider the set term $\{x:x \neq x \wedge A \}$ a *logical variant* of $\{x:x \neq x \}$ if $A$ is a tautology of predicate logic. Given such notions of alphabetical and logical variants, one may consider $\{x:x \neq x \wedge A \}$ an *alphabetological* variant of $\{y:y \neq y\}$.

Do my notions of *logical variant* and *alphabetological variant* have provenances?