Theorem hba1w

Description: 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)

	Ref	Expression
Hypothesis	hbn1w.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	hba1w	$$⊢\forall x\phi \to \forall x\forall x\phi$$

Proof

Step	Hyp	Ref	Expression
1		hbn1w.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
2	1	cbvalvw	$$⊢\forall x\phi \leftrightarrow \forall y\psi$$
3	2	notbii	$$⊢\neg \forall x\phi \leftrightarrow \neg \forall y\psi$$
4	3	a1i	$$⊢x=y\to \left(\neg \forall x\phi \leftrightarrow \neg \forall y\psi \right)$$
5	4	spw	$$⊢\forall x\neg \forall x\phi \to \neg \forall x\phi$$
6	5	con2i	$$⊢\forall x\phi \to \neg \forall x\neg \forall x\phi$$
7	4	hbn1w	$$⊢\neg \forall x\neg \forall x\phi \to \forall x\neg \forall x\neg \forall x\phi$$
8	1	hbn1w	$$⊢\neg \forall x\phi \to \forall x\neg \forall x\phi$$
9	8	con1i	$$⊢\neg \forall x\neg \forall x\phi \to \forall x\phi$$
10	9	alimi	$$⊢\forall x\neg \forall x\neg \forall x\phi \to \forall x\forall x\phi$$
11	6 7 10	3syl	$$⊢\forall x\phi \to \forall x\forall x\phi$$