Theorem alexn

A relationship between two quantifiers and negation. (Contributed by NM, 18-Aug-1993.)

Conclusion
\( \vdash \forall x \, \exists y \, \neg \varphi \leftrightarrow \neg \exists x \, \forall y \, \varphi \)
Proof
exnal
l1
albii _
\( \vdash \forall x \, \exists y \, \neg \varphi \leftrightarrow \forall x \, \neg \forall y \, \varphi \)
alnex
\( \vdash \forall x \, \neg \forall y \, \varphi \leftrightarrow \neg \exists x \, \forall y \, \varphi \)
bitri l1 _