Theorem hbn1

Alias for [ax-10] to be used instead of it. (Contributed by NM, 24-Jan-1993.) (Proof shortened by Wolf Lammen, 18-Aug-2014.)

Conclusion

\( \vdash \neg \forall x \, \varphi \rightarrow \forall x \, \neg \forall x \, \varphi \)

Proof

ax-10