Theorem bj-cbvaw 37244

Description: Universally quantifying over a non-occurring variable is independent from the variable, under a weaker condition than in bj-cbvalvv 37242. 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 1857	. . 3 ⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)
2		bj-cbvalvv 37242	. . 3 ⊢ (∃𝑥 ¬ 𝜑 → (∀𝑥𝜓 → ∀𝑦𝜓))
3	1, 2	sylbir 238	. 2 ⊢ (¬ ∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑦𝜓))
4		falim 1587	. . . 4 ⊢ (⊥ → 𝜓)
5	4	alimi 1841	. . 3 ⊢ (∀𝑦⊥ → ∀𝑦𝜓)
6	5	a1d 26	. 2 ⊢ (∀𝑦⊥ → (∀𝑥𝜓 → ∀𝑦𝜓))
7	3, 6	ja 188	1 ⊢ ((∀𝑥𝜑 → ∀𝑦⊥) → (∀𝑥𝜓 → ∀𝑦𝜓))

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1568  ⊥wfal 1582  ∃wex 1809

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-tru 1573  df-fal 1583  df-ex 1810

This theorem is referenced by: (None)