Theorem hbn1fw
Weak version of [ax-10] from which we can prove any [ax-10] instance not
involving wff variables or bundling. Uses only Tarski's FOL axiom
schemes. (Contributed by NM, 19-Apr-2017.) (Proof shortened by Wolf
Lammen, 28-Feb-2018.)
Hypotheses
hbn1fw.1
\( \vdash \forall x \, \varphi \rightarrow \forall y \, \forall x \, \varphi \)
hbn1fw.2
\( \vdash \neg \psi \rightarrow \forall x \, \neg \psi \)
hbn1fw.3
\( \vdash \forall y \, \psi \rightarrow \forall x \, \forall y \, \psi \)
hbn1fw.4
\( \vdash \neg \varphi \rightarrow \forall y \, \neg \varphi \)
hbn1fw.5
\( \vdash \neg \forall y \, \psi \rightarrow \forall x \, \neg \forall y \, \psi \)
hbn1fw.6
\( \vdash x = y \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \neg \forall x \, \varphi \rightarrow \forall x \, \neg \forall x \, \varphi \)
Proof
l0
hbn1fw.1
l1
hbn1fw.2
l2
hbn1fw.3
l3
hbn1fw.4
hbn1fw.6
cbvalw l0 l1 l2 l3 _
l6
notbii _
\( \vdash \neg \forall x \, \varphi \leftrightarrow \neg \forall y \, \psi \)
hbn1fw.5
\( \vdash \neg \forall y \, \psi \rightarrow \forall x \, \neg \forall y \, \psi \)
hbxfrbi l6 _