Theorem empty

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

	Ref	Expression
Assertion	empty	$$⊢\neg \exists x\top \leftrightarrow \forall x\perp$$

Proof

Step	Hyp	Ref	Expression
1		df-fal	$$⊢\perp \leftrightarrow \neg \top$$
2	1	albii	$$⊢\forall x\perp \leftrightarrow \forall x\neg \top$$
3		alnex	$$⊢\forall x\neg \top \leftrightarrow \neg \exists x\top$$
4	2 3	bitr2i	$$⊢\neg \exists x\top \leftrightarrow \forall x\perp$$