Theorem ax13dgen2

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

Conclusion
\( \vdash \neg x = y' \rightarrow y' = x \rightarrow \forall x \, y' = x \)
Proof
l0
equcomi
\( \vdash y' = x \rightarrow x = y' \)
pm2.21
\( \vdash \neg x = y' \rightarrow x = y' \rightarrow \forall x \, y' = x \)
syl5 l0 _