A formula that uses a uniqueness quantifier expresses that there exists one and only one number with a particular property. For example, (E! x (= (* (2) x) (6))) means that there exists some number x for which (= (* (2) x) (6)) and no other numbers satisfy this property. Uniqueness quantifiers are part of predicate calculus.
The uniqueness quantifier is defined as (<-> (E! x ph) (E. y (A. x (<-> ph (= x y))))) /edit/peano_new/predicate/equality.gh/df-eu.