Theorem hbn1fw

Description: Weak version of ax-10 from which we can prove any ax-10 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)

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

Proof

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