Theorem ax13lem1

A version of ax13v with one distinct variable restriction dropped. For convenience, \( y' \) is kept on the right side of equations. The proof of ax13 bases on ideas from NM, 24-Dec-2015. (Contributed by Wolf Lammen, 8-Sep-2018.) (New usage is discouraged.)

Conclusion
\( \vdash \neg x = y' \rightarrow z' = y' \rightarrow \forall x \, z' = y' \)
Proof
l0
equvinva
\( \vdash z' = y' \rightarrow \exists w \, (z' = w \wedge y' = w) \)
l1
ax13v
\( \vdash \neg x = y' \rightarrow y' = w \rightarrow \forall x \, y' = w \)
equeucl
alimdv _
\( \vdash z' = w \rightarrow \forall x \, y' = w \rightarrow \forall x \, z' = y' \)
syl9 l1 _
impd _
exlimdv _
\( \vdash \neg x = y' \rightarrow \exists w \, (z' = w \wedge y' = w) \rightarrow \forall x \, z' = y' \)
syl5 l0 _