Unique existential and at-most-one quantifiers (#2843)
Unique existential and at-most-one quantifiers (#2843)

* standardize: 'unique existential quantifier' for E! and 'at-most-one quantifier' for E*; standardize: unicity-->uniqueness

* typos

* document quantifiers in ~conventions
metamath/set.mm,metamath/set.mm,metamath/set.mm