Theorem emptyal

On the empty domain, any universally quantified formula is true. (Contributed by Wolf Lammen, 12-Mar-2023.)

Conclusion
\( \vdash \neg \exists x \, \top \rightarrow \forall x \, \varphi \)
Proof
l0
emptyex
\( \vdash \neg \exists x \, \top \rightarrow \neg \exists x \, \neg \varphi \)
alex
\( \vdash \forall x \, \varphi \leftrightarrow \neg \exists x \, \neg \varphi \)
sylibr l0 _