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	⊢ ( ( ∃ 𝑥 ⊤ → ∃ 𝑦 𝜑 ) → ( ∀ 𝑦 𝜓 → ∀ 𝑥 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		empty	⊢ ( ¬ ∃ 𝑥 ⊤ ↔ ∀ 𝑥 ⊥ )
2		falim	⊢ ( ⊥ → 𝜓 )
3	2	alimi	⊢ ( ∀ 𝑥 ⊥ → ∀ 𝑥 𝜓 )
4	3	a1d	⊢ ( ∀ 𝑥 ⊥ → ( ∀ 𝑦 𝜓 → ∀ 𝑥 𝜓 ) )
5	1 4	sylbi	⊢ ( ¬ ∃ 𝑥 ⊤ → ( ∀ 𝑦 𝜓 → ∀ 𝑥 𝜓 ) )
6		bj-cbvalvv	⊢ ( ∃ 𝑦 𝜑 → ( ∀ 𝑦 𝜓 → ∀ 𝑥 𝜓 ) )
7	5 6	ja	⊢ ( ( ∃ 𝑥 ⊤ → ∃ 𝑦 𝜑 ) → ( ∀ 𝑦 𝜓 → ∀ 𝑥 𝜓 ) )