Description: There exists at most one empty set. With either axnul or axnulALT or ax-nul , this proves that there exists a unique empty set. In
practice, once the language of classes is available, we use the stronger
characterization among classes eq0 . (Contributed by NM, 22-Dec-2007) Use the at-most-one quantifier. (Revised by BJ, 17-Sep-2022)(Proof shortened by Wolf Lammen, 26-Apr-2023)