Description: Definition of the uniqueness quantifier which is correct on the empty
domain. Instead of the fresh variable z , one could save a dummy
variable by using x or y at the cost of having nested
quantifiers on the same variable. (Contributed by BJ, 12-Mar-2023)