# 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}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
hbn1fw.2 ${⊢}¬{\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}¬{\psi }$
hbn1fw.3 ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}{\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\psi }$
hbn1fw.4 ${⊢}¬{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}¬{\phi }$
hbn1fw.5 ${⊢}¬\forall {y}\phantom{\rule{.4em}{0ex}}{\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {y}\phantom{\rule{.4em}{0ex}}{\psi }$
hbn1fw.6 ${⊢}{x}={y}\to \left({\phi }↔{\psi }\right)$
Assertion hbn1fw ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$

### Proof

Step Hyp Ref Expression
1 hbn1fw.1 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 hbn1fw.2 ${⊢}¬{\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}¬{\psi }$
3 hbn1fw.3 ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}{\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\psi }$
4 hbn1fw.4 ${⊢}¬{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}¬{\phi }$
5 hbn1fw.5 ${⊢}¬\forall {y}\phantom{\rule{.4em}{0ex}}{\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {y}\phantom{\rule{.4em}{0ex}}{\psi }$
6 hbn1fw.6 ${⊢}{x}={y}\to \left({\phi }↔{\psi }\right)$
7 1 2 3 4 6 cbvalw ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {y}\phantom{\rule{.4em}{0ex}}{\psi }$
8 7 notbii ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }↔¬\forall {y}\phantom{\rule{.4em}{0ex}}{\psi }$
9 8 5 hbxfrbi ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$