The only way I could think of to do this problem is reductio, but since the two biconditional terms are not contradictory, I am pretty stuck.
E(x,y) <-> ¬ E(y,y) is clearly false if x and y are the same, because then the statement becomes E(x,x) <-> ¬ E(x,x).
Whatever we choose for x, E(x,y) <-> ¬ E(y,y) is not true for all y, because it is not true for y = x.
Here is a proof using the law of excluded middle. After eliminating the existential quantifier to get x, apply the universal quantification on x itself to get E(x,x) ↔ ¬E(x,x). This is false if E(x,x) is true or false.
Variable P : Prop -> Prop -> Prop. Axiom LEM : forall p, p \/ ~p. Goal ~exists x, forall y, (P x y -> ~P y y) /\ (~P y y -> P x y). intro. elim H. intros. assert (P x x \/ ~P x x) by apply LEM. elim H1; intro. apply H0 with x; assumption. apply H0 with x; apply H0; assumption. Qed.