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?