Strange tendency to turn the Drinker Paradox into a Russell Paradox

[Jean-Luc-Picard-2021]

Was using Exy as a shorthand for set membership x e y. Was looking at this proof:

∃x(Exy → ∀zEzy) is valid. https://www.umsu.de/trees/#~7x%28Exy~5~6zEzy%29

In step 3 it shows Eyy. Could this not also be Eby? How does it choose y?

[Jean-Luc-Picard-2021]

The Naoyuki Tamura seqprover for classical first-order logic invents a new variables, no Russell Paradox, which would read d(d):

------------------------------------------- Ax-c d(X1),d(Z) --> d(X1),d(Y1),X#(d(X)->Y@d(Y)) -------------------------------------------- R@ d(X1),d(Z) --> d(X1),Y@d(Y),X#(d(X)->Y@d(Y)) --------------------------------------------- R-> d(Z) --> d(X1),d(X1)->Y@d(Y),X#(d(X)->Y@d(Y)) --------------------------------------------- R#-c d(Z) --> d(X1),X#(d(X)->Y@d(Y)) -------------------------------- R@ d(Z) --> Y@d(Y),X#(d(X)->Y@d(Y)) ---------------------------------- R-> --> d(Z)->Y@d(Y),X#(d(X)->Y@d(Y)) ---------------------------------- R#-c --> X#(d(X)->Y@d(Y)) ------------------------ Ltop top --> X#(d(X)->Y@d(Y))

https://www.vidal-rosset.net/g4-prover/g4action.php?formula=top+--%3E+X%23%28d%28X%29-%3EY%40d%28Y%29%29+&sysopt=g4c&output=pretty