Theorem ax13dgen3

Degenerate instance of [ax-13] where bundled variables \( y' \) 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' = y' \rightarrow \forall x \, y' = y' \)
Proof
equid
ax-gen _
2a1i _