The Stanford Encyclopaedia entry on Free Logic gives the following axiomatisation of first-order free logic using an "existence predicate" E!
(A1) All tautologies
(A2) $A\rightarrow\forall xA, x\text{ not free in} A$
(A3) $\forall x(A \rightarrow B) \rightarrow (\forall xA \rightarrow \forall xB)$
(A4) $\forall xA(x/t), \text{ if } A \text{ is an axiom}$
(A5) $\forall xA \rightarrow (E!t \rightarrow A(t/x))$
(A6) $\forall x E!x$
It then notes that if we expand the language by introducing the identity sign "=" with the usual axioms, viz
(A7) $s=t \rightarrow(A \rightarrow A(t//s))$
(A8) $\forall x(x=x)$
the existence predicate "E!" may then be defined by
$E!t =_{def}\exists y(y=t)$
My question is whether this definition makes axiom (A6) redundant; that is, is $\forall x\exists y(x=y)$ derivable from (A1)-(A5) + (A7)-(A8). It seems to me like it ought to be, but I haven't managed to find a proof.
Thanks!