Theorem empty

Two characterizations of the empty domain. (Contributed by Gérard Lang, 5-Feb-2024.)

Conclusion
\( \vdash \neg \exists x \, \top \leftrightarrow \forall x \, \bot \)
Proof
df-fal
l1
albii _
\( \vdash \forall x \, \bot \leftrightarrow \forall x \, \neg \top \)
alnex
\( \vdash \forall x \, \neg \top \leftrightarrow \neg \exists x \, \top \)
bitr2i l1 _