Description: Define the existential uniqueness quantifier. This expresses unique
existence, or existential uniqueness, which is the conjunction of
existence ( df-ex ) and uniqueness ( df-mo ). The expression
E! x ph is read "there exists exactly one x such that ph " or
"there exists a unique x such that ph ". This is also called the
"uniqueness quantifier" but that expression is also used for the
at-most-one quantifier df-mo , therefore we avoid that ambiguous name.

Definition 10.1 of BellMachover p. 97; also Definition *14.02 of
WhiteheadRussell p. 175. Other possible definitions are given by
eu1 , eu2 , eu3v , and eu6 . As for double unique existence,
beware that the expression E! x E! y ph means "there exists a unique
x such that there exists a unique y such that ph " which is a
weaker property than "there exists exactly one x and one y such
that ph " (see 2eu4 ). (Contributed by NM, 12-Aug-1993) Make this
the definition (which used to be eu6 , while this definition was then
proved as dfeu ). (Revised by BJ, 30-Sep-2022)