Theorem bj-cbveaw

Description: Universally quantifying over a non-occurring variable is independent from the variable, under a weaker condition than in bj-cbvalvv . (Contributed by BJ, 14-Mar-2026) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		empty	$$⊢\neg \exists x\top \leftrightarrow \forall x\perp$$
2		falim	$$⊢\perp \to \psi$$
3	2	alimi	$$⊢\forall x\perp \to \forall x\psi$$
4	3	a1d	$$⊢\forall x\perp \to \left(\forall y\psi \to \forall x\psi \right)$$
5	1 4	sylbi	$$⊢\neg \exists x\top \to \left(\forall y\psi \to \forall x\psi \right)$$
6		bj-cbvalvv	$$⊢\exists y\phi \to \left(\forall y\psi \to \forall x\psi \right)$$
7	5 6	ja	$$⊢\left(\exists x\top \to \exists y\phi \right)\to \left(\forall y\psi \to \forall x\psi \right)$$