Theorem bj-cbvaw 36877

Description: Universally quantifying over a non-occurring variable is independent from the variable, under a weaker condition than in bj-cbvalvv 36875. 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 186); an intuitionistically valid statement is obtained by expressing the antecedent as a disjunction (classically equivalent through imor 854). (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 1829	. . 3 ⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)
2		bj-cbvalvv 36875	. . 3 ⊢ (∃𝑥 ¬ 𝜑 → (∀𝑥𝜓 → ∀𝑦𝜓))
3	1, 2	sylbir 235	. 2 ⊢ (¬ ∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑦𝜓))
4		falim 1559	. . . 4 ⊢ (⊥ → 𝜓)
5	4	alimi 1813	. . 3 ⊢ (∀𝑦⊥ → ∀𝑦𝜓)
6	5	a1d 25	. 2 ⊢ (∀𝑦⊥ → (∀𝑥𝜓 → ∀𝑦𝜓))
7	3, 6	ja 186	1 ⊢ ((∀𝑥𝜑 → ∀𝑦⊥) → (∀𝑥𝜓 → ∀𝑦𝜓))

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1540  ⊥wfal 1554  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-tru 1545  df-fal 1555  df-ex 1782

This theorem is referenced by: (None)