Theorem hbn1w
Weak version of hbn1. Uses only Tarski's FOL axiom schemes.
(Contributed by NM, 9-Apr-2017.)
Hypothesis
hbn1w.1
\( \vdash x = y \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \neg \forall x \, \varphi \rightarrow \forall x \, \neg \forall x \, \varphi \)
Proof
l0
ax-5
\( \vdash \forall x \, \varphi \rightarrow \forall y \, \forall x \, \varphi \)
l1
ax-5
\( \vdash \neg \psi \rightarrow \forall x \, \neg \psi \)
l2
ax-5
\( \vdash \forall y \, \psi \rightarrow \forall x \, \forall y \, \psi \)
l3
ax-5
\( \vdash \neg \varphi \rightarrow \forall y \, \neg \varphi \)
l4
ax-5
\( \vdash \neg \forall y \, \psi \rightarrow \forall x \, \neg \forall y \, \psi \)
hbn1w.1
\( \vdash x = y \rightarrow (\varphi \leftrightarrow \psi) \)
hbn1fw l0 l1 l2 l3 l4 _