Theorem ax13w

Weak version (principal instance) of [ax-13]. (Because \( y' \) and \( z' \) don't need to be distinct, this actually bundles the principal instance and the degenerate instance \( \neg x = y' \rightarrow y' = y' \rightarrow \forall x \, y' = y' \) .) Uses only Tarski's FOL axiom schemes. The proof is trivial but is included to complete the set ax10w, ax11w, and ax12w. (Contributed by NM, 10-Apr-2017.)

Conclusion
\( \vdash \neg x = y' \rightarrow y' = z' \rightarrow \forall x \, y' = z' \)
Proof
ax5d