Theorem bj-cbvaw 37632

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4  ∀wal 1567  ⊥wfal 1581  ∃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-tru 1572  df-fal 1582  df-ex 1812

This theorem is used by: (None)