I'd be wary of using $\forall !$ as your notation for this. (See here for example.) The word 'unique' definitely doesn't mean what you want to say, though. 'Unique' means 'one', and 'distinct' means... exactly the opposite!
You'd be better off writing "for all distinct $x,y \in S$".
Working formally, if you were trying to show that a property $\phi(x,y)$ holds for distinct $x,y \in S$ you could write
$$(\forall x,y \in S)(x \ne y \to \phi(x,y))$$
...but outside of logic there isn't really much need for this kind of notation.
I think that there is no "compact" formalization of the required double substitution.
Assuming that [using $v_0, v_1, v_2$] :
$\varphi (v_1) := \forall v_0 \psi(v_0, v_1)$
we have :
$\forall v_0 \psi(v_0, v_1)[v_0 ← v_2] \equiv \forall v_2 \psi(v_2, v_1)$
with $v_2$ a new variable. This condition licences us to prove the equivalence.
Now we can perform the second substitution :
$\varphi (v_0) := \forall v_2 \psi(v_2, v_1)[v_1 ← v_0]$.
But, in general :
$\varphi(v_1) \nvdash \varphi(v_0)$.
We can try with the approach to substitution in John Bell & Moshe Machover, A Course in Mathematical Logic (1977), page 57-on.
The "syntax" for substitution is : $\alpha(x,t)$ and the basic defintion is Definition 3.3 [page 59] :
We shall say that $t$ is free to be substituted for $x$ in $\alpha$ (briefly, free for
$x$ in $\alpha$) if no free occurrence of $x$ in $\alpha$ is within a subformula of $\alpha$ having the form $\forall y \beta$ where $y$ occurs in $t$.
If $t$ is free for $x$ in $\alpha$, we shall define $\alpha(x/t)$ as the result of substituting an occurrence of $t$ for each free occurrence of $x$ in $\alpha$.
Definition 3.5 [page 61]. If $z$ is a variable which is not free in $\beta$ but is free for $x$ in $\beta$, we say that $\forall z [\beta(x/z)]$ arises from $\forall x \beta$ by (correct) alphabetic change. (Note that if $z$ does not occur at all in $\beta$, then $z$ certainly satisfies both of the above conditions.)
Thus, considering again the formula :
$\varphi := \forall v_0 \psi(v_0, v_1, v_2)$
we perform an alphabetic change using $v_n$, where $v_n$ is the first variable not occurring in $\varphi$, getting :
$\forall v_n [\psi(v_0/v_n, v_1, v_2)]$
and then the substitution : $v_1 ← v_0$ (now $v_0$ is free for $v_1$ in the formula), to get :
$\forall v_n [\psi(v_0/v_n, v_1/v_0, v_2)]$.
The result will be :
$\varphi' := \forall v_n \psi(v_n, v_0, v_2)$.
Best Answer
The phrase is simply "there exists", notated $\exists$.
In English, if you wanted to emphasize that you don't mean "there exists a unique ...", then you might say "there exists at least one ...".
Symbolically, there should be no need for this emphasis.