Theorem bj-cbvaw 37077

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1557  ⊥wfal 1571  ∃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-tru 1562  df-fal 1572  df-ex 1799

This theorem is referenced by: (None)