Theorem hbnaev

Any variable is free in \( \neg \forall x \, x = y' \), if \( x \) and \( y' \) are distinct. This condition is dropped in hbnae, at the expense of more axiom dependencies. Instance of naev2. (Contributed by NM, 13-May-1993.) (Revised by Wolf Lammen, 9-Apr-2021.)

Conclusion

\( \vdash \neg \forall x \, x = y' \rightarrow \forall z \, \neg \forall x \, x = y' \)

Proof

naev2

\( \vdash \neg \forall x \, x = y' \rightarrow \forall z \, \neg \forall w \, w = y' \)

naev

\( \vdash \neg \forall w \, w = y' \rightarrow \neg \forall x \, x = y' \)

alimi _

syl l0 _