Definition df-bj-diag 32266

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 32265	. 2 class Diag
2		vx	. . 3 setvar 𝑥
3		cvv 3173	. . 3 class V
4		cid 4948	. . . 4 class I
5	2	cv 1474	. . . . 5 class 𝑥
6	5, 5	cxp 5036	. . . 4 class (𝑥 × 𝑥)
7	4, 6	cin 3539	. . 3 class ( I ∩ (𝑥 × 𝑥))
8	2, 3, 7	cmpt 4643	. 2 class (𝑥 ∈ V ↦ ( I ∩ (𝑥 × 𝑥)))
9	1, 8	wceq 1475	1 wff Diag = (𝑥 ∈ V ↦ ( I ∩ (𝑥 × 𝑥)))

This definition is referenced by:  bj-diagval  32267