Theorem bj-cbvaew

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

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

Proof

Step	Hyp	Ref	Expression
1		notnotb	$$⊢\phi \leftrightarrow \neg \neg \phi$$
2	1	albii	$$⊢\forall x\phi \leftrightarrow \forall x\neg \neg \phi$$
3		df-fal	$$⊢\perp \leftrightarrow \neg \top$$
4	3	albii	$$⊢\forall y\perp \leftrightarrow \forall y\neg \top$$
5	2 4	imbi12i	$$⊢\left(\forall x\phi \to \forall y\perp \right)\leftrightarrow \left(\forall x\neg \neg \phi \to \forall y\neg \top \right)$$
6		bj-exexalal	$$⊢\left(\exists y\top \to \exists x\neg \phi \right)\leftrightarrow \left(\forall x\neg \neg \phi \to \forall y\neg \top \right)$$
7	5 6	bitr4i	$$⊢\left(\forall x\phi \to \forall y\perp \right)\leftrightarrow \left(\exists y\top \to \exists x\neg \phi \right)$$
8		bj-cbvew	$$⊢\left(\exists y\top \to \exists x\neg \phi \right)\to \left(\exists y\psi \to \exists x\psi \right)$$
9	7 8	sylbi	$$⊢\left(\forall x\phi \to \forall y\perp \right)\to \left(\exists y\psi \to \exists x\psi \right)$$