Theorem bj-cbvew 36983

Description: Existentially quantifying over a non-occurring variable is independent from the variable, under a weaker condition than in bj-cbvexvv 36981. 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 1557	. . . . 5 ⊢ (𝜓 → ⊤)
2	1	eximi 1842	. . . 4 ⊢ (∃𝑥𝜓 → ∃𝑥⊤)
3		pm3.35 808	. . . 4 ⊢ ((∃𝑥⊤ ∧ (∃𝑥⊤ → ∃𝑦𝜑)) → ∃𝑦𝜑)
4	2, 3	sylan 586	. . 3 ⊢ ((∃𝑥𝜓 ∧ (∃𝑥⊤ → ∃𝑦𝜑)) → ∃𝑦𝜑)
5		bj-cbvexvv 36981	. . . 4 ⊢ (∃𝑦𝜑 → (∃𝑥𝜓 → ∃𝑦𝜓))
6	5	impcom 408	. . 3 ⊢ ((∃𝑥𝜓 ∧ ∃𝑦𝜑) → ∃𝑦𝜓)
7	4, 6	syldan 597	. 2 ⊢ ((∃𝑥𝜓 ∧ (∃𝑥⊤ → ∃𝑦𝜑)) → ∃𝑦𝜓)
8	7	expcom 414	1 ⊢ ((∃𝑥⊤ → ∃𝑦𝜑) → (∃𝑥𝜓 → ∃𝑦𝜓))

Syntax hints:   → wi 4  ⊤wtru 1548  ∃wex 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787

This theorem is referenced by:  bj-cbvaew  36985