Theorem ax13
Derive [ax-13] from ax13v and Tarski's FOL. This shows that the
weakening in ax13v is still sufficient for a complete system.
Preferably, use the weaker ax13w to avoid the propagation of [ax-13].
(Contributed by NM, 21-Dec-2015.) (Proof shortened by Wolf Lammen,
31-Jan-2018.) Reduce axiom usage. (Revised by Wolf Lammen,
2-Jun-2021.) (New usage is discouraged.)
Conclusion
\( \vdash \neg x = y' \rightarrow y' = z' \rightarrow \forall x \, y' = z' \)
Proof
l0
equvinv
\( \vdash y' = z' \leftrightarrow \exists w \, (w = y' \wedge w = z') \)
ax13lem1
l2
imp _
\( \vdash \neg x = y' \wedge w = y' \rightarrow \forall x \, w = y' \)
ax13lem1
l4
imp _
\( \vdash \neg x = z' \wedge w = z' \rightarrow \forall x \, w = z' \)
ax7v1
imp _
alanimi _
\( \vdash \forall x \, w = y' \wedge \forall x \, w = z' \rightarrow \forall x \, y' = z' \)
syl2an l2 l4 _
an4s _
ex _
exlimdv _
\( \vdash \neg x = y' \wedge \neg x = z' \rightarrow \exists w \, (w = y' \wedge w = z') \rightarrow \forall x \, y' = z' \)
biimtrid l0 _
l13
ex _
\( \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 l13 _