Can antisymmetry $x\rho y\;\land\;y\rho x\;\implies x=y$ be rewritten

Question

Can antisymmetry $x\rho y\;\land\;y\rho x\implies x=y$ be rewritten as $(x\rho y\;\land x\ne y)\implies\neg(y\rho x)$ and hold when $x\ne y$ and we have $x\rho y\veebar x\rho y$ May I ask anybody for explanation?

Answer 1

This is how I would approach such a problem. $$\begin{array}{ccr} &xRy \,\land\, yRx \Rightarrow x=y &\\ \Leftrightarrow & \neg (xRy \,\land\, yRx) \lor x=y & (A\Rightarrow B\equiv \neg A \lor B) \\ \Leftrightarrow &\neg (xRy) \lor \neg (yRx) \lor x=y & (\text{Duality})\\ \Leftrightarrow & \neg (xRy) \lor x=y \lor \neg(yRx) & (\text{Commutativity of } \lor) \\ \Leftrightarrow & \neg (xRy \land x\neq y) \lor \neg(yRx) & (\text{Duality}) \\ \Leftrightarrow & xRy \,\land\,x\neq y \Rightarrow \neg(yRx) & ( A\Rightarrow B\equiv \neg A \lor B) \end{array}$$ By duality I mean De Morgan's laws, more precisely, here we're using $\neg (A\land B) \equiv \neg A\lor \neg B$. If one is pedantic enough, they should also note that we're using associativity of $\lor$.