Theorem bj-hbext

Description: Closed form of hbex . (Contributed by BJ, 10-Oct-2019)

	Ref	Expression
Assertion	bj-hbext	$$⊢\forall y\forall x\left(\phi \to \forall x\phi \right)\to \left(\exists y\phi \to \forall x\exists y\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		nfa2	$$⊢Ⅎx\forall y\forall x\left(\phi \to \forall x\phi \right)$$
2		hbnt	$$⊢\forall x\left(\phi \to \forall x\phi \right)\to \left(\neg \phi \to \forall x\neg \phi \right)$$
3	2	alimi	$$⊢\forall y\forall x\left(\phi \to \forall x\phi \right)\to \forall y\left(\neg \phi \to \forall x\neg \phi \right)$$
4		bj-hbalt	$$⊢\forall y\left(\neg \phi \to \forall x\neg \phi \right)\to \left(\forall y\neg \phi \to \forall x\forall y\neg \phi \right)$$
5	3 4	syl	$$⊢\forall y\forall x\left(\phi \to \forall x\phi \right)\to \left(\forall y\neg \phi \to \forall x\forall y\neg \phi \right)$$
6	1 5	alrimi	$$⊢\forall y\forall x\left(\phi \to \forall x\phi \right)\to \forall x\left(\forall y\neg \phi \to \forall x\forall y\neg \phi \right)$$
7		hbnt	$$⊢\forall x\left(\forall y\neg \phi \to \forall x\forall y\neg \phi \right)\to \left(\neg \forall y\neg \phi \to \forall x\neg \forall y\neg \phi \right)$$
8	6 7	syl	$$⊢\forall y\forall x\left(\phi \to \forall x\phi \right)\to \left(\neg \forall y\neg \phi \to \forall x\neg \forall y\neg \phi \right)$$
9		df-ex	$$⊢\exists y\phi \leftrightarrow \neg \forall y\neg \phi$$
10	9	bicomi	$$⊢\neg \forall y\neg \phi \leftrightarrow \exists y\phi$$
11	10	albii	$$⊢\forall x\neg \forall y\neg \phi \leftrightarrow \forall x\exists y\phi$$
12	8 10 11	3imtr3g	$$⊢\forall y\forall x\left(\phi \to \forall x\phi \right)\to \left(\exists y\phi \to \forall x\exists y\phi \right)$$