# Metamath Proof Explorer

## Theorem hbn1w

Description: Weak version of hbn1 . Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017)

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