Metamath Proof Explorer


Theorem empty

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

Ref Expression
Assertion empty ¬xx

Proof

Step Hyp Ref Expression
1 df-fal ¬
2 1 albii xx¬
3 alnex x¬¬x
4 2 3 bitr2i ¬xx