The z would be completely redundant. This is because 'what you're doing with z', i.e. (Wz → z=x), is the same as what you're doing with y, and they are both from the same set; that is, every z could've been y and vice versa. This together means every case of z is already caught by y.
There is a very intuitive mathematical rule that says that we can change the name of bound variables (variables can be bound by existential or universal quantification). Basically, it means that the following two are equivalent:
'x' or 'y' are just names, and they don't carry meaning.
There is another rule that says we can swap universal quantifications as we like, such that the following two are equivalent:
- (x)(y)(P(x) ∧ Q(y))
- (y)(x)(P(x) ∧ Q(y))
Note that this is not the same rule as above, i.e. we didn't rename x to y and vice versa, because the inner experssion "P(x) ∧ Q(y)" doesn't change. Only the order of the quantifications is changed.
Intuitively, these two together show that we may rename the z you added to y, yielding:
(x)(Wx → (y)(y)(Wy → y=x) ∧ (Wy → y=x))
Note: this is no good notation, because the y's are ambiguous. This is just to give you the idea of the intuitive notion.
On both sides of the ∧ we have the same expression, so we can simplify it:
(x)(Wx → (y)(y)(Wy → y=x))
And then we can also remove one of the y's...
(x)(Wx → (y)(Wy → y=x))
Bringing us back to the initial expression.