I suspect the solution lies in the phrase "in fact empty". The empty relation is trivially well founded. So look at why set membership for y should be the empty relation. I'll take a shot (with the caveat that I'm no logician, and I'm not entirely convinced by this argument myself).

It might be helpful first to remove x from the picture and define y as: y = {{y}} and y \neq {y}

First note that there can be at most one distinct member of {{y}}, which is {y}. So if there exists z member of y, then z = {y}. Then y is a member of z, and by transitivity, y is member of y, and so y = z = {y}. This contradicts the assumption that y \neq {y}, so there can be no such z.

I took that class from Kunen at Wisconsin in the late 80s. But I'll be damned if I can find my copy of that yellow book or remember enough to be of any help.

I have to admit that I never really did understand forcing.

It seemed like all the logic professors at UW at that time, including Kunen, were getting interested in computer science.

Kleene was still around at that time, too.