Description: Alternate version of Russell's definition of a description binder, which
can be read as "the unique x such that ph ", where ph
ordinarily contains x as a free variable. Our definition is
meaningful only when there is exactly one x such that ph is true
(see aiotaval ); otherwise, it is not a set (see aiotaexb ), or even
more concrete, it is the universe _V (see aiotavb ). Since this
is an alternative for df-iota , we call this symbol iota'alternate iota in the following.

The advantage of this definition is the clear distinguishability of the
defined and undefined cases: the alternate iota over a wff is defined
iff it is a set (see aiotaexb ). With the original definition, there
is no corresponding theorem ( E! x ph <-> ( iota x ph ) =/= (/) ) ,
because (/) can be a valid unique set satisfying a wff (see, for
example, iota0def ). Only the right to left implication would hold,
see (negated) iotanul . For defined cases, however, both definitions
df-iota and df-aiota are equivalent, see reuaiotaiota . (Proposed
by BJ, 13-Aug-2022.) (Contributed by AV, 24-Aug-2022)