Natural Deduction with Identity

Question

I am confused on how to deal with identities in natural deduction proofs with predicate logic. More specifically, how would one go about solving this?

∀x(Fx → x = a)
     ¬Ga
---------------
 ∀x(Gx → ¬Fx)

The idenity rules I have are:

| c = c    =I

and

m | c = d
n | Ac
  | Ad     =E m,n

Answer 1

Hint: Assume $Gy$. Assume $Fy$. Then $y=a$, so $Ga$, contradiction. Thus $\lnot Fy$. Conclude $\forall x(Gx\to\lnot Fx)$. I'll leave it to you to translate this proof sketch into your formal natural deduction system.