**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 iotaval 6071);
otherwise, it evaluates to the empty set (see iotanul 6075). Russell used
the inverted iota symbol ℩ 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
riotacl2 6844 (or iotacl 6083 for unbounded iota), as demonstrated in the
proof of supub 8600. This can be easier than applying riotasbc 6846 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.
(Contributed by Andrew Salmon, 30-Jun-2011.) |