Prove that $\forall x \forall y (A(x,y) \rightarrow \neg A(y,x)) \vdash \forall x \forall y (A(x,y) \rightarrow \neg x = y)$

Question

In predicate logic how to prove that:

$$\forall x \forall y (A(x,y) \rightarrow \neg A(y,x)) \vdash \forall x \forall y (A(x,y) \rightarrow \neg x = y)$$

First it should be proven that:

$$x=y \vdash A(x,y)\leftrightarrow A(y,x) $$

(I did prove the second result, but have problems utilizing it).

Answer 1

Hint

1) $∀x∀y(A(x,y)→¬A(y,x))$ --- premise

From it derive : $A(x,x)→¬A(x,x)$ and with TAUT : $(P \to \lnot P) \to \lnot P$ derive : $\lnot A(x,x)$.

2) $A(x,y)$ --- assumed [a]

3) $x=y$ --- assumed [b]

From 2) and 3) derive : $A(x,x)$ --- contradicition !

Conclude with : $¬x=y$, discharging [b].

Derive : $A(x,y) \to ¬x=y$, discharging [a].