Theorem bj-cbvaw 37125

Description: Universally quantifying over a non-occurring variable is independent from the variable, under a weaker condition than in bj-cbvalvv 37123. If ⊥ is substituted for 𝜑, then the statement reads: "universally quantifying over a non-occurring variable is independent from the variable as soon as that result is true for the False truth constant". The label "cbvaw" means "'change bound variable' theorem, 'all' quantifier, weak version". (Contributed by BJ, 14-Mar-2026.) This proof is not intuitionistic (it uses ja 188); an intuitionistically valid statement is obtained by expressing the antecedent as a disjunction (classically equivalent through imor 866). (Proof modification is discouraged.)

Assertion

Ref	Expression
bj-cbvaw	⊢ ((∀𝑥𝜑 → ∀𝑦⊥) → (∀𝑥𝜓 → ∀𝑦𝜓))

Distinct variable groups:   𝜓,𝑥   𝜓,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem bj-cbvaw

Step	Hyp	Ref	Expression
1		exnal 1850	. . 3 ⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)
2		bj-cbvalvv 37123	. . 3 ⊢ (∃𝑥 ¬ 𝜑 → (∀𝑥𝜓 → ∀𝑦𝜓))
3	1, 2	sylbir 238	. 2 ⊢ (¬ ∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑦𝜓))
4		falim 1580	. . . 4 ⊢ (⊥ → 𝜓)
5	4	alimi 1834	. . 3 ⊢ (∀𝑦⊥ → ∀𝑦𝜓)
6	5	a1d 26	. 2 ⊢ (∀𝑦⊥ → (∀𝑥𝜓 → ∀𝑦𝜓))
7	3, 6	ja 188	1 ⊢ ((∀𝑥𝜑 → ∀𝑦⊥) → (∀𝑥𝜓 → ∀𝑦𝜓))

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1561  ⊥wfal 1575  ∃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-tru 1566  df-fal 1576  df-ex 1803

This theorem is referenced by: (None)