Theorem ax13ALT

Alternate proof of ax13 from FOL, sp, and axc9. (Contributed by NM, 21-Dec-2015.) (Proof shortened by Wolf Lammen, 31-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash \neg x = y' \rightarrow y' = z' \rightarrow \forall x \, y' = z' \)
Proof
sp
l1
con3i _
\( \vdash \neg x = y' \rightarrow \neg \forall x \, x = y' \)
sp
l3
con3i _
\( \vdash \neg x = z' \rightarrow \neg \forall x \, x = z' \)
axc9
\( \vdash \neg \forall x \, x = y' \rightarrow \neg \forall x \, x = z' \rightarrow y' = z' \rightarrow \forall x \, y' = z' \)
l5
syl2im l1 l3 _
\( \vdash \neg x = y' \rightarrow \neg x = z' \rightarrow y' = z' \rightarrow \forall x \, y' = z' \)
ax13b
\( \vdash \neg x = y' \rightarrow y' = z' \rightarrow \forall x \, y' = z' \leftrightarrow \neg x = y' \rightarrow \neg x = z' \rightarrow y' = z' \rightarrow \forall x \, y' = z' \)
mpbir l5 _