Theorem 2exnaln

Theorem *11.22 in [WhiteheadRussell] p. 160. (Contributed by Andrew Salmon, 24-May-2011.)

Conclusion
\( \vdash \exists x \, \exists y \, \varphi \leftrightarrow \neg \forall x \, \forall y \, \neg \varphi \)
Proof
l0
df-ex
\( \vdash \exists x \, \exists y \, \varphi \leftrightarrow \neg \forall x \, \neg \exists y \, \varphi \)
alnex
albii _
\( \vdash \forall x \, \forall y \, \neg \varphi \leftrightarrow \forall x \, \neg \exists y \, \varphi \)
xchbinxr l0 _