Theorem bj-cbvew 37078

Description: Existentially quantifying over a non-occurring variable is independent from the variable, under a weaker condition than in bj-cbvexvv 37076. 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 1569	. . . . 5 ⊢ (𝜓 → ⊤)
2	1	eximi 1854	. . . 4 ⊢ (∃𝑥𝜓 → ∃𝑥⊤)
3		pm3.35 812	. . . 4 ⊢ ((∃𝑥⊤ ∧ (∃𝑥⊤ → ∃𝑦𝜑)) → ∃𝑦𝜑)
4	2, 3	sylan 589	. . 3 ⊢ ((∃𝑥𝜓 ∧ (∃𝑥⊤ → ∃𝑦𝜑)) → ∃𝑦𝜑)
5		bj-cbvexvv 37076	. . . 4 ⊢ (∃𝑦𝜑 → (∃𝑥𝜓 → ∃𝑦𝜓))
6	5	impcom 411	. . 3 ⊢ ((∃𝑥𝜓 ∧ ∃𝑦𝜑) → ∃𝑦𝜓)
7	4, 6	syldan 600	. 2 ⊢ ((∃𝑥𝜓 ∧ (∃𝑥⊤ → ∃𝑦𝜑)) → ∃𝑦𝜓)
8	7	expcom 417	1 ⊢ ((∃𝑥⊤ → ∃𝑦𝜑) → (∃𝑥𝜓 → ∃𝑦𝜓))

Syntax hints:   → wi 4  ⊤wtru 1560  ∃wex 1798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799

This theorem is referenced by:  bj-cbvaew  37080