Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bj-diag Structured version   Visualization version   GIF version

Definition df-bj-diag 33419
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
StepHypRef Expression
1 cdiag2 33418 . 2 class Diag
2 vx . . 3 setvar 𝑥
3 cvv 3349 . . 3 class V
4 cid 5156 . . . 4 class I
52cv 1629 . . . . 5 class 𝑥
65, 5cxp 5247 . . . 4 class (𝑥 × 𝑥)
74, 6cin 3720 . . 3 class ( I ∩ (𝑥 × 𝑥))
82, 3, 7cmpt 4861 . 2 class (𝑥 ∈ V ↦ ( I ∩ (𝑥 × 𝑥)))
91, 8wceq 1630 1 wff Diag = (𝑥 ∈ V ↦ ( I ∩ (𝑥 × 𝑥)))
Colors of variables: wff setvar class
This definition is referenced by:  bj-diagval  33420
  Copyright terms: Public domain W3C validator