This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ \forall x φ \to \forall y \forall x φ$
		hbn1fw.2	$⊢ \neg ψ \to \forall x \neg ψ$
		hbn1fw.3	$⊢ \forall y ψ \to \forall x \forall y ψ$
		hbn1fw.4	$⊢ \neg φ \to \forall y \neg φ$
		hbn1fw.5	$⊢ \neg \forall y ψ \to \forall x \neg \forall y ψ$
		hbn1fw.6	$⊢ x = y \to (φ \leftrightarrow ψ)$
	Assertion	hbn1fw	$⊢ \neg \forall x φ \to \forall x \neg \forall x φ$

Proof

Step	Hyp	Ref	Expression
1		hbn1fw.1	$⊢ \forall x φ \to \forall y \forall x φ$
2		hbn1fw.2	$⊢ \neg ψ \to \forall x \neg ψ$
3		hbn1fw.3	$⊢ \forall y ψ \to \forall x \forall y ψ$
4		hbn1fw.4	$⊢ \neg φ \to \forall y \neg φ$
5		hbn1fw.5	$⊢ \neg \forall y ψ \to \forall x \neg \forall y ψ$
6		hbn1fw.6	$⊢ x = y \to (φ \leftrightarrow ψ)$
7	1 2 3 4 6	cbvalw	$⊢ \forall x φ \leftrightarrow \forall y ψ$
8	7	notbii	$⊢ \neg \forall x φ \leftrightarrow \neg \forall y ψ$
9	8 5	hbxfrbi	$⊢ \neg \forall x φ \to \forall x \neg \forall x φ$