Theorem emptynf

On the empty domain, any variable is effectively nonfree in any formula. (Contributed by Wolf Lammen, 12-Mar-2023.)

Conclusion
\( \vdash \neg \exists x \, \top \rightarrow \Finv x \, \varphi \)
Proof
l0
emptyal
\( \vdash \neg \exists x \, \top \rightarrow \forall x \, \varphi \)
nftht
\( \vdash \forall x \, \varphi \rightarrow \Finv x \, \varphi \)
syl l0 _