Is this alternative definition of 'equivalence relation' correct?

Question

I was puzzling over another question: Let $R$ be an equivalence relation on a set $A$, $a,b \in A$. Prove $[a] = [b]$ iff $aRb$. And this made me discover that $$(0) \; \langle \forall a,b :: aRb \equiv \langle \forall x :: aRx \equiv bRx \rangle \rangle$$ is an alternative characterization of $R$ being an equivalence relation, and one which only uses logical equivalence. (Note that throughout this question, $a$, $b$, $c$, and $x$ implicitly range over a fixed set $A$.)

Update 3: To put it more explicitly and longwindedly, I discovered that $$R \textrm{ is an equivalence relation on } A \;\equiv\; \langle \forall a,b \in A :: aRb \:\equiv\: \langle \forall x \in A :: aRx \equiv bRx\rangle \rangle$$

(I've updated this question to ask for the correctness of this definition, and have posted my original question as a separate one: Is this alternative definition of 'equivalence relation' well-known? useful? used?)

The nice thing about this definition is that it says, "equivalence of $a$ and $b$ means that it doesn't matter which of the two you substitute", which seems to be the essence of equivalence (cf. Leibniz' law).

Is this alternative definition well-known? useful? used? correct?

---

Update: Two comments and one answer suggest that my $(0)$ is not equivalent to the combination of \begin{align} (1) & \langle \forall a :: aRa \rangle \\ (2) & \langle \forall a,b :: aRb \;\Rightarrow\; bRa \rangle \\ (3) & \langle \forall a,b,c :: aRb \land bRc \;\Rightarrow\; aRc \rangle \\ \end{align} However, as far as I can see these are equivalent. One direction is proven in the answers to the question referenced above. For the other direction, we have for all $a$ \begin{align} & aRa \\ \equiv & \;\;\;\;\;\text{"using $(0)$ with $b:=a$"} \\ & \langle \forall x :: aRx \equiv aRx \rangle \\ \equiv & \;\;\;\;\;\text{"logic"} \\ & \textrm{true} \\ \end{align} and for all $a$ and $b$ \begin{align} & aRb \\ \equiv & \;\;\;\;\;\text{"by $(0)$"} \\ & \langle \forall x :: aRx \equiv bRx \rangle \\ \Rightarrow & \;\;\;\;\;\text{"choose $x:=a$"} \\ & aRa \equiv bRa \\ \equiv & \;\;\;\;\;\text{"by $(1)$"} \\ & bRa \\ \end{align} and for all $a$, $b$, and $c$ \begin{align} & aRb \land bRc \\ \equiv & \;\;\;\;\;\text{"by $(0)$, twice"} \\ & \langle \forall x :: aRx \equiv bRx \rangle \land \langle \forall x :: bRx \equiv cRx \rangle \\ \Rightarrow & \;\;\;\;\;\text{"logic"} \\ & \langle \forall x :: aRx \equiv cRx \rangle \\ \equiv & \;\;\;\;\;\text{"by $(0)$ with $b:=c$"} \\ & aRc \\ \end{align}

Or am I missing something?

---

Update 2: In the above I have now made all quantifications explicit, to prevent any confusion.

Answer 1

What you have almost works. The only problem with it is that it makes $R$ a proper class, since it implies that $xRx$ for all sets $x$. You really ought to quantify over the domain of $R$; if that’s $D$, you want

$$\forall x,y\Big(xRy\leftrightarrow x,y\in D\land\forall z\in D(xRz\leftrightarrow yRz)\Big)\;.$$

Now you get $xRx$ precisely for those sets $x$ that are elements of $D$, which is what you want.

Answer 2

Your characterization of $R$ may "beg the question": the characterization of an equivalence relation:$$aRb \equiv \langle \forall x :: aRx \equiv bRx \rangle$$

works fine, provided we know that $R$ is reflexive. So if you're trying to define an equivalence relation, we run into problems.

However, if you have the added premise: "given $R$ is an equivalence relation," then indeed, $R$ is reflexive. So if you are offering an alternative characterization of what it means for two elements to be related under $R$, given that $\,R\,$ is an equivalence relation, then I think your characterization is fine, and is appealing at an intuitive level. However, you'll want to restrict $x$ to the domain (set $S$) on which the equivalence relations $R$ is defined, and also add the qualification that $a, b \in S$. $$a, b \in S \land aRb \equiv (\forall x \in S :: aRx \equiv bRx)$$