I'm sorry, but this post is utterly pedantic.

The proof by Daniel Levine is absolutely "logically sound." The idea that what was shown was the conditional, "if y=y then x0=0" and not "x0=0 is true" simply ignores the fact that the first proposition in the proof was NOT an implication or derivation - it was an axiom.

Because it is an axiom, we are guaranteed that the argument is sound (and the conclusion true under whatever interpretation allows proposition #1 as an axiom) as soon as we prove that the argument is valid. Which is exactly what Levine set out to show. Logic 101.