Theorem bj-cbvew 37305

Description: Existentially quantifying over a non-occurring variable is independent from the variable, under a weaker condition than in bj-cbvexvv 37303. If ⊤ is substituted for 𝜑, 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.)

Assertion

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

Distinct variable groups:   𝜓,𝑥   𝜓,𝑦

Allowed substitution hints:   𝜑(𝑥, 𝑦)

Proof of Theorem bj-cbvew

Step	Hyp	Ref	Expression
1		trud 1580	. . . . 5 ⊢ (𝜓 → ⊤)
2	1	eximi 1868	. . . 4 ⊢ (∃𝑥𝜓 → ∃𝑥⊤)
3		pm3.35 815	. . . 4 ⊢ ((∃𝑥⊤ ∧ (∃𝑥⊤ → ∃𝑦𝜑)) → ∃𝑦𝜑)
4	2, 3	sylan 592	. . 3 ⊢ ((∃𝑥𝜓 ∧ (∃𝑥⊤ → ∃𝑦𝜑)) → ∃𝑦𝜑)
5		bj-cbvexvv 37303	. . . 4 ⊢ (∃𝑦𝜑 → (∃𝑥𝜓 → ∃𝑦𝜓))
6	5	impcom 413	. . 3 ⊢ ((∃𝑥𝜓 ∧ ∃𝑦𝜑) → ∃𝑦𝜓)
7	4, 6	syldan 603	. 2 ⊢ ((∃𝑥𝜓 ∧ (∃𝑥⊤ → ∃𝑦𝜑)) → ∃𝑦𝜓)
8	7	expcom 419	1 ⊢ ((∃𝑥⊤ → ∃𝑦𝜑) → (∃𝑥𝜓 → ∃𝑦𝜓))

This proof depends on syntax axioms:   → wi 4  ⊤wtru 1571  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813

This theorem is used by:  bj-cbvaew  37307