Theorem bj-exexalal

Description: A lemma for changing bound variables. Only the forward implication is intuitionistic. (Contributed by BJ, 14-Mar-2026)

	Ref	Expression
Assertion	bj-exexalal	⊢ ( ( ∃ 𝑥 𝜑 → ∃ 𝑦 𝜓 ) ↔ ( ∀ 𝑦 ¬ 𝜓 → ∀ 𝑥 ¬ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		con34b	⊢ ( ( ∃ 𝑥 𝜑 → ∃ 𝑦 𝜓 ) ↔ ( ¬ ∃ 𝑦 𝜓 → ¬ ∃ 𝑥 𝜑 ) )
2		alnex	⊢ ( ∀ 𝑦 ¬ 𝜓 ↔ ¬ ∃ 𝑦 𝜓 )
3		alnex	⊢ ( ∀ 𝑥 ¬ 𝜑 ↔ ¬ ∃ 𝑥 𝜑 )
4	2 3	imbi12i	⊢ ( ( ∀ 𝑦 ¬ 𝜓 → ∀ 𝑥 ¬ 𝜑 ) ↔ ( ¬ ∃ 𝑦 𝜓 → ¬ ∃ 𝑥 𝜑 ) )
5	1 4	bitr4i	⊢ ( ( ∃ 𝑥 𝜑 → ∃ 𝑦 𝜓 ) ↔ ( ∀ 𝑦 ¬ 𝜓 → ∀ 𝑥 ¬ 𝜑 ) )