# Metamath Proof Explorer

## Theorem naev2

Description: Generalization of hbnaev . (Contributed by Wolf Lammen, 9-Apr-2021)

Ref Expression
Assertion naev2 ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \forall {z}\phantom{\rule{.4em}{0ex}}¬\forall {t}\phantom{\rule{.4em}{0ex}}{t}={u}$

### Proof

Step Hyp Ref Expression
1 naev ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to ¬\forall {v}\phantom{\rule{.4em}{0ex}}{v}={w}$
2 ax-5 ${⊢}¬\forall {v}\phantom{\rule{.4em}{0ex}}{v}={w}\to \forall {z}\phantom{\rule{.4em}{0ex}}¬\forall {v}\phantom{\rule{.4em}{0ex}}{v}={w}$
3 naev ${⊢}¬\forall {v}\phantom{\rule{.4em}{0ex}}{v}={w}\to ¬\forall {t}\phantom{\rule{.4em}{0ex}}{t}={u}$
4 3 alimi ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}¬\forall {v}\phantom{\rule{.4em}{0ex}}{v}={w}\to \forall {z}\phantom{\rule{.4em}{0ex}}¬\forall {t}\phantom{\rule{.4em}{0ex}}{t}={u}$
5 1 2 4 3syl ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \forall {z}\phantom{\rule{.4em}{0ex}}¬\forall {t}\phantom{\rule{.4em}{0ex}}{t}={u}$