Theorem bj-cbvew 37126

Description: Existentially quantifying over a non-occurring variable is independent from the variable, under a weaker condition than in bj-cbvexvv 37124. 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 1573	. . . . 5 ⊢ (𝜓 → ⊤)
2	1	eximi 1858	. . . 4 ⊢ (∃𝑥𝜓 → ∃𝑥⊤)
3		pm3.35 814	. . . 4 ⊢ ((∃𝑥⊤ ∧ (∃𝑥⊤ → ∃𝑦𝜑)) → ∃𝑦𝜑)
4	2, 3	sylan 591	. . 3 ⊢ ((∃𝑥𝜓 ∧ (∃𝑥⊤ → ∃𝑦𝜑)) → ∃𝑦𝜑)
5		bj-cbvexvv 37124	. . . 4 ⊢ (∃𝑦𝜑 → (∃𝑥𝜓 → ∃𝑦𝜓))
6	5	impcom 412	. . 3 ⊢ ((∃𝑥𝜓 ∧ ∃𝑦𝜑) → ∃𝑦𝜓)
7	4, 6	syldan 602	. 2 ⊢ ((∃𝑥𝜓 ∧ (∃𝑥⊤ → ∃𝑦𝜑)) → ∃𝑦𝜓)
8	7	expcom 418	1 ⊢ ((∃𝑥⊤ → ∃𝑦𝜑) → (∃𝑥𝜓 → ∃𝑦𝜓))

Syntax hints:   → wi 4  ⊤wtru 1564  ∃wex 1802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803

This theorem is referenced by:  bj-cbvaew  37128