Theorem bj-cbvew

Description: Existentially quantifying over a non-occurring variable is independent from the variable, under a weaker condition than in bj-cbvexvv . If T. is substituted for ph , then the statement reads: "existentially quantifying over a non-occurring variable is independent from the variable as soon as that result is true for the True truth constant. The label "cbvew" means "'change bound variable' theorem, 'exists' quantifier, weak version". (Contributed by BJ, 14-Mar-2026) This proof is intuitionistic. (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-cbvew	⊢ ( ( ∃ 𝑥 ⊤ → ∃ 𝑦 𝜑 ) → ( ∃ 𝑥 𝜓 → ∃ 𝑦 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		trud	⊢ ( 𝜓 → ⊤ )
2	1	eximi	⊢ ( ∃ 𝑥 𝜓 → ∃ 𝑥 ⊤ )
3		pm3.35	⊢ ( ( ∃ 𝑥 ⊤ ∧ ( ∃ 𝑥 ⊤ → ∃ 𝑦 𝜑 ) ) → ∃ 𝑦 𝜑 )
4	2 3	sylan	⊢ ( ( ∃ 𝑥 𝜓 ∧ ( ∃ 𝑥 ⊤ → ∃ 𝑦 𝜑 ) ) → ∃ 𝑦 𝜑 )
5		bj-cbvexvv	⊢ ( ∃ 𝑦 𝜑 → ( ∃ 𝑥 𝜓 → ∃ 𝑦 𝜓 ) )
6	5	impcom	⊢ ( ( ∃ 𝑥 𝜓 ∧ ∃ 𝑦 𝜑 ) → ∃ 𝑦 𝜓 )
7	4 6	syldan	⊢ ( ( ∃ 𝑥 𝜓 ∧ ( ∃ 𝑥 ⊤ → ∃ 𝑦 𝜑 ) ) → ∃ 𝑦 𝜓 )
8	7	expcom	⊢ ( ( ∃ 𝑥 ⊤ → ∃ 𝑦 𝜑 ) → ( ∃ 𝑥 𝜓 → ∃ 𝑦 𝜓 ) )