Theorem alex

Universal quantifier in terms of existential quantifier and negation. Dual of [df-ex]. See also the dual pair alnex / exnal. Theorem 19.6 of [Margaris] p. 89. (Contributed by NM, 12-Mar-1993.)

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