Theorem emptyal

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

	Ref	Expression
Assertion	emptyal	$$⊢\neg \exists x\top \to \forall x\phi$$

Proof

Step	Hyp	Ref	Expression
1		emptyex	$$⊢\neg \exists x\top \to \neg \exists x\neg \phi$$
2		alex	$$⊢\forall x\phi \leftrightarrow \neg \exists x\neg \phi$$
3	1 2	sylibr	$$⊢\neg \exists x\top \to \forall x\phi$$