Theorem hba1w
Weak version of hba1. See comments for ax10w. Uses only Tarski's
FOL axiom schemes. (Contributed by NM, 9-Apr-2017.) (Proof shortened
by Wolf Lammen, 10-Oct-2021.)
Hypothesis
hbn1w.1
\( \vdash x = y \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \forall x \, \varphi \rightarrow \forall x \, \forall x \, \varphi \)
Proof
hbn1w.1
cbvalvw _
notbii _
l3
a1i _
\( \vdash x = y \rightarrow (\neg \forall x \, \varphi \leftrightarrow \neg \forall y \, \psi) \)
spw _
l5
con2i _
\( \vdash \forall x \, \varphi \rightarrow \neg \forall x \, \neg \forall x \, \varphi \)
l6
hbn1w l3
\( \vdash \neg \forall x \, \neg \forall x \, \varphi \rightarrow \forall x \, \neg \forall x \, \neg \forall x \, \varphi \)
hbn1w.1
\( \vdash x = y \rightarrow (\varphi \leftrightarrow \psi) \)
hbn1w _
con1i _
alimi _
\( \vdash \forall x \, \neg \forall x \, \neg \forall x \, \varphi \rightarrow \forall x \, \forall x \, \varphi \)
3syl l5 l6 _