Description: Define Russell's
definition description binder, which can be read as
"the unique such that ," where ordinarily contains
as a free variable. Our definition is meaningful
only when there
is exactly one such that is true (see iotaval5475);
otherwise, it evaluates to the empty set (see iotanul5479). Russell used
the inverted iota symbol iota to
represent the binder.

Sometimes proofs need to expand an iota-based definition. That is,
given "X = the x for which ... x ... x ..." holds, the proof
needs to
get to "... X ... X ...". A general strategy to do this is
to use
riotacl26613 (or iotacl5487 for unbounded iota), as demonstrated in the
proof of supub7513. This can be easier than applying riotasbc6615 or a
version that applies an explicit substitution, because substituting an
iota into its own property always has a bound variable clash which must
be first renamed or else guarded with NF.