Definition df-bj-diag

Description: Define the functionalized identity, which can also be seen as the diagonal function. Its value is given in bj-diagval when it is viewed as the functionalized identity, and in bj-diagval2 when it is viewed as the diagonal function.

Indeed, Definition df-br identifies a binary relation with the class of couples that are related by that binary relation (see eqrel2 for the extensionality property of binary relations). As a consequence, the identity relation, or identity function (see funi ), 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 .

Note: most proofs will only use its values (IdA ) , in which case it may be enough to use ` ( I |`A ) everywhere and dispense with this definition. (Contributed by BJ, 22-Jun-2019)

	Ref	Expression
Assertion	df-bj-diag	|- _Id = ( x e. _V |-> ( _I |` x ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdiag2	|- _Id
1		vx	|- x
2		cvv	|- _V
3		cid	|- _I
4	1	cv	|- x
5	3 4	cres	|- ( _I |` x )
6	1 2 5	cmpt	|- ( x e. _V |-> ( _I |` x ) )
7	0 6	wceq	|- _Id = ( x e. _V |-> ( _I |` x ) )