Description: The class of sets verifying a property is the empty class if and only if
that property is a contradiction. See also abn0 (from which it could be
proved using as many essential proof steps but one fewer syntactic step,
at the cost of depending on df-ne ). (Contributed by BJ, 19-Mar-2021)