**Description: **Define the functionalized
identity, which can also be seen as the diagonal
function. Its value is given in bj-diagval 34605 when it is viewed as the
functionalized identity, and in bj-diagval2 34606 when it is viewed as the
diagonal function.
Indeed, Definition df-br 5031 identifies a binary relation with the class
of
couples that are related by that binary relation (see eqrel2 35733 for the
extensionality property of binary relations). As a consequence, the
identity relation, or identity function (see funi 6356), on any class, can
alternatively be seen as the diagonal of the cartesian square of that
class.
The identity relation on the universal class, I,
is an "identity
relation generator", since its restriction to any class is the
identity
relation on that class. It may be useful to consider a functionalized
version of that fact, and that is the purpose of df-bj-diag 34604.
Note: most proofs will only use its values (Id‘𝐴), in which
case it may be enough to use ( I ↾ 𝐴) everywhere and dispense
with
this definition. (Contributed by BJ,
22-Jun-2019.) |