Theorem hbn1fw 2046

Description: Weak version of ax-10 2142 from which we can prove any ax-10 2142 instance not involving wff variables or bundling. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 19-Apr-2017.) (Proof shortened by Wolf Lammen, 28-Feb-2018.)

Hypotheses

Ref	Expression
hbn1fw.1	⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑)
hbn1fw.2	⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓)
hbn1fw.3	⊢ (∀𝑦𝜓 → ∀𝑥∀𝑦𝜓)
hbn1fw.4	⊢ (¬ 𝜑 → ∀𝑦 ¬ 𝜑)
hbn1fw.5	⊢ (¬ ∀𝑦𝜓 → ∀𝑥 ¬ ∀𝑦𝜓)
hbn1fw.6	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
hbn1fw	⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑)

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦)

Proof of Theorem hbn1fw

Step	Hyp	Ref	Expression
1		hbn1fw.1	. . . 4 ⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑)
2		hbn1fw.2	. . . 4 ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓)
3		hbn1fw.3	. . . 4 ⊢ (∀𝑦𝜓 → ∀𝑥∀𝑦𝜓)
4		hbn1fw.4	. . . 4 ⊢ (¬ 𝜑 → ∀𝑦 ¬ 𝜑)
5		hbn1fw.6	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
6	1, 2, 3, 4, 5	cbvalw 2035	. . 3 ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)
7	6	notbii 320	. 2 ⊢ (¬ ∀𝑥𝜑 ↔ ¬ ∀𝑦𝜓)
8		hbn1fw.5	. 2 ⊢ (¬ ∀𝑦𝜓 → ∀𝑥 ¬ ∀𝑦𝜓)
9	7, 8	hbxfrbi 1825	1 ⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206  ∀wal 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780

This theorem is referenced by:  hbn1w  2047