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 = (𝑥 ∈ V ↦ ( I ∩ (𝑥 × 𝑥)))

Detailed syntax breakdown of Definition df-bj-diag

Step	Hyp	Ref	Expression
1		cdiag2 33088	. 2 class Diag
2		vx	. . 3 setvar 𝑥
3		cvv 3200	. . 3 class V
4		cid 5023	. . . 4 class I
5	2	cv 1482	. . . . 5 class 𝑥
6	5, 5	cxp 5112	. . . 4 class (𝑥 × 𝑥)
7	4, 6	cin 3573	. . 3 class ( I ∩ (𝑥 × 𝑥))
8	2, 3, 7	cmpt 4729	. 2 class (𝑥 ∈ V ↦ ( I ∩ (𝑥 × 𝑥)))
9	1, 8	wceq 1483	1 wff Diag = (𝑥 ∈ V ↦ ( I ∩ (𝑥 × 𝑥)))

This definition is referenced by:  bj-diagval  33090