Theorem ax13dgen1

Degenerate instance of [ax-13] where bundled variables \( x \) and \( y \) have a common substitution. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 13-Apr-2017.)

Conclusion
\( \vdash \neg x = x \rightarrow x = z' \rightarrow \forall x \, x = z' \)
Proof
equid
pm2.24i _