Theorem bj-cbvew 37634

Description: Existentially quantifying over a non-occurring variable is independent from the variable, under a weaker condition than in bj-cbvexvv 37632. 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 1579	. . . . 5 ⊢ (𝜓 → ⊤)
2	1	eximi 1867	. . . 4 ⊢ (∃𝑥𝜓 → ∃𝑥⊤)
3		pm3.35 815	. . . 4 ⊢ ((∃𝑥⊤ ∧ (∃𝑥⊤ → ∃𝑦𝜑)) → ∃𝑦𝜑)
4	2, 3	sylan 592	. . 3 ⊢ ((∃𝑥𝜓 ∧ (∃𝑥⊤ → ∃𝑦𝜑)) → ∃𝑦𝜑)
5		bj-cbvexvv 37632	. . . 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 1570  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812

This theorem is used by:  bj-cbvaew  37636