Okay, this is freaking me out, I'm going nuts. In a first-order condition with formula $\phi$ containing $x, y$ such as
$\forall x\forall y . \phi$
I need to ensure that the second variable bound by the universal quantifier can only take values that are distinct from those of the first variable bound by the first universal quantifier respectively, but I do not know how to write this down cleanly as a formula. I need something like
$\forall x\in D\,\forall y\in D-\{x\}.\phi$
but this does not seem to be the proper way of writing it down either (although I've seen this in CS papers). It mixes up variables with their interpretation and only hints at the intended dependence. You might think that the textbook restriction
$\forall x\,\forall y. x\neq y\to\phi$
would do the trick but it doesn't seem to work. If $x=y$, then the condition ought to be false or undefined, but not vacuously true. However, $\phi$ contains an anti-reflexive relation, so with unrestricted quantification the whole condition could never be true, which is not right either. I rather need this: "The condition is true if for all distinct $x$ and $y$, $\phi$ is true, otherwise it is false." - but as a formula, not as paraphrase!
I've looked up branching quantifiers and IF logic, but they seem to do the opposite, allowing one to express independence between quantifiers rather than additional dependencies. I suspect I have overlooked something very basic and simple, but what?
If the goal is to avoid a model with only one element, why not just prepend $(\exists x)(\exists y)[x \not = y]$ to the front, and then use the definition that you like for models that have more than one element?