Prove the following:proving formula in predicate logic

Question

(∀y)(∀x)(¬=∨=)→(∀x)(¬=∨=)

I am using Mathematical Logic by Dr. Tourlakis. My try:

(∀x)(¬=∨=)

¬((∀y))(∀x)(¬=∨=) )∨(∀x)(¬=∨=) <1+A⊢B∨A>

(∀y)(∀x)(¬=∨=)→(∀x)(¬=∨=)<3+implication theorem +equation>

How can I prove this one ? Is my answer correct and accurate to you?

Answer 1

Hint

Assume the antecedent : $(∀y)(∀x)(\lnot (x=y) \lor x=y)$ and apply Ax2 [page 139] : $(\forall x)A \to A[x := t]$ twice to get :

$\lnot (t=t) \lor t=t$,

where term $t$ is free for $y$ and $x$ [see page 133 : every term different from $x$ and $y$ will do].

Then use 6.1.1 (Weak Generalization) [page 155] to get :

$(∀x)(\lnot (x=x) \lor x=x)$.

Finally, use 2.6.1 (Deduction Theorem) [page 81].