Definition df-bj-diag 33089

Description: Define the diagonal of the Cartesian square of a set. (Contributed by BJ, 22-Jun-2019.)

Assertion

Ref	Expression
df-bj-diag	|- Diag = ( x e. _V |-> ( _I i^i ( x X. x ) ) )

Detailed syntax breakdown of Definition df-bj-diag

Step	Hyp	Ref	Expression
1		cdiag2 33088	. 2 class Diag
2		vx	. . 3 setvar x
3		cvv 3200	. . 3 class _V
4		cid 5023	. . . 4 class _I
5	2	cv 1482	. . . . 5 class x
6	5, 5	cxp 5112	. . . 4 class ( x X. x )
7	4, 6	cin 3573	. . 3 class ( _I i^i ( x X. x ) )
8	2, 3, 7	cmpt 4729	. 2 class ( x e. _V |-> ( _I i^i ( x X. x ) ) )
9	1, 8	wceq 1483	1 wff Diag = ( x e. _V |-> ( _I i^i ( x X. x ) ) )

This definition is referenced by:  bj-diagval  33090