Quantifier elimination for theory of equivalence relations

Question

Let $\mathcal{L}=\{\sim\}$ and $\Sigma_\infty$ be the set of axioms stating that:

(i) $\sim$ is an equivalence relation
(ii) Every equivalence class is infinite
(iii) there are infinitely many equivalence classes

It suffices to show that every $\mathcal{L}$ formula $\exists y\varphi(x,y)$ is $\Sigma_\infty$-equivalent to a quantifier free $\psi(x)$, where $x=(x_1,\ldots,x_n)$ are distinct variables, and $\varphi(x,y)$ is a conjunction of literals. Since it's fairly trivial when $\varphi(x,y)$ has a conjunct of the form $x_i=y$, we can assume we need to reduce $$\exists y (\bigwedge_{i\in I} x_i\not=y\wedge\bigwedge_{j\in J}x_j\sim y\wedge\bigwedge_{h\in H}\neg (x_j\sim y))$$ My question is whether or not the following condition holds:

$$\Sigma_\infty\vdash\exists y (\bigwedge_{i\in I} x_i\not=y\wedge\bigwedge_{j\in J}x_j\sim y\wedge\bigwedge_{h\in H}\neg (x_j\sim y))\leftrightarrow(\bigwedge_{j\in J,h\in H}\neg(x_i\sim x_j)\wedge\bigwedge_{j,j'\in J}x_j\sim x_{j'})$$ I can't think of a reason why it would not, but I'm a bit worried about ignoring the information about non-identical elements in the unreduced formula.

Answer 1

The equivalence holds because the equivalence classes are infinite. If you have $(x_1,…,x_n)$ such that the RHS holds, the set $\{x_j \mid j\in J\}$ is finite. If it is nonempty, there is an element $y$ such that $y\sim x_j$ for $j\in J$ and $y\neq x_j$. If the set is empty, the existence of $y$ is implied by the fact that there are infinitely many equivalence classes, so you can pick a $y$ that is not $\sim$-equivalent to any $x_h,h\in H$.