Theorem empty

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

	Ref	Expression
Assertion	empty	⊢ ( ¬ ∃ 𝑥 ⊤ ↔ ∀ 𝑥 ⊥ )

Proof

Step	Hyp	Ref	Expression
1		df-fal	⊢ ( ⊥ ↔ ¬ ⊤ )
2	1	albii	⊢ ( ∀ 𝑥 ⊥ ↔ ∀ 𝑥 ¬ ⊤ )
3		alnex	⊢ ( ∀ 𝑥 ¬ ⊤ ↔ ¬ ∃ 𝑥 ⊤ )
4	2 3	bitr2i	⊢ ( ¬ ∃ 𝑥 ⊤ ↔ ∀ 𝑥 ⊥ )