Theorem nfeqf2
An equation between setvar is free of any other setvar. Usage of this
theorem is discouraged because it depends on [ax-13]. (Contributed by
Wolf Lammen, 9-Jun-2019.) Remove dependency on [ax-12]. (Revised by
Wolf Lammen, 16-Dec-2022.) (New usage is discouraged.)
Conclusion
\( \vdash \neg \forall x \, x = y' \rightarrow \Finv x \, z' = y' \)
Proof
l0
exnal
\( \vdash \exists x \, \neg x = y' \leftrightarrow \neg \forall x \, x = y' \)
l1
hbe1
l2
ax13lem2
\( \vdash \neg x = y' \rightarrow \exists x \, z' = y' \rightarrow z' = y' \)
ax13lem1
\( \vdash \neg x = y' \rightarrow z' = y' \rightarrow \forall x \, z' = y' \)
syldc l2 _
l5
eximdh l1 _
\( \vdash \exists x \, z' = y' \rightarrow \exists x \, \neg x = y' \rightarrow \exists x \, \forall x \, z' = y' \)
hbe1a
\( \vdash \exists x \, \forall x \, z' = y' \rightarrow \forall x \, z' = y' \)
syl6com l5 _
nfd _
\( \vdash \exists x \, \neg x = y' \rightarrow \Finv x \, z' = y' \)
sylbir l0 _