Theorem ax13lem2
Lemma for nfeqf2. This lemma is equivalent to ax13v with one
distinct variable constraint removed. (Contributed by Wolf Lammen,
8-Sep-2018.) Reduce axiom usage. (Revised by Wolf Lammen,
18-Oct-2020.) (New usage is discouraged.)
Conclusion
\( \vdash \neg x = y' \rightarrow \exists x \, z' = y' \rightarrow z' = y' \)
Proof
l0
ax13lem1
\( \vdash \neg x = y' \rightarrow w = y' \rightarrow \forall x \, w = y' \)
equeucl
l2
eximi _
\( \vdash \exists x \, z' = y' \rightarrow \exists x \, (w = y' \rightarrow z' = w) \)
19.36v
\( \vdash \exists x \, (w = y' \rightarrow z' = w) \leftrightarrow \forall x \, w = y' \rightarrow z' = w \)
sylib l2 _
\( \vdash \exists x \, z' = y' \rightarrow \forall x \, w = y' \rightarrow z' = w \)
syl9 l0 _
l6
alrimdv _
\( \vdash \neg x = y' \rightarrow \exists x \, z' = y' \rightarrow \forall w \, (w = y' \rightarrow z' = w) \)
equequ2
equsalvw _
\( \vdash \forall w \, (w = y' \rightarrow z' = w) \leftrightarrow z' = y' \)
imbitrdi l6 _