Definition df-uvtx 27753

Description: Define the class of all universal vertices (in graphs). A vertex is called universal if it is adjacent, i.e. connected by an edge, to all other vertices (of the graph), or equivalently, if all other vertices are its neighbors. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 24-Oct-2020.)

Assertion

Ref	Expression
df-uvtx	⊢ UnivVtx = (𝑔 ∈ V ↦ {𝑣 ∈ (Vtx‘𝑔) ∣ ∀𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣})𝑛 ∈ (𝑔 NeighbVtx 𝑣)})

Distinct variable group:   𝑣,𝑔,𝑛

Detailed syntax breakdown of Definition df-uvtx

Step	Hyp	Ref	Expression
1		cuvtx 27752	. 2 class UnivVtx
2		vg	. . 3 setvar 𝑔
3		cvv 3432	. . 3 class V
4		vn	. . . . . . 7 setvar 𝑛
5	4	cv 1538	. . . . . 6 class 𝑛
6	2	cv 1538	. . . . . . 7 class 𝑔
7		vv	. . . . . . . 8 setvar 𝑣
8	7	cv 1538	. . . . . . 7 class 𝑣
9		cnbgr 27699	. . . . . . 7 class NeighbVtx
10	6, 8, 9	co 7275	. . . . . 6 class (𝑔 NeighbVtx 𝑣)
11	5, 10	wcel 2106	. . . . 5 wff 𝑛 ∈ (𝑔 NeighbVtx 𝑣)
12		cvtx 27366	. . . . . . 7 class Vtx
13	6, 12	cfv 6433	. . . . . 6 class (Vtx‘𝑔)
14	8	csn 4561	. . . . . 6 class {𝑣}
15	13, 14	cdif 3884	. . . . 5 class ((Vtx‘𝑔) ∖ {𝑣})
16	11, 4, 15	wral 3064	. . . 4 wff ∀𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣})𝑛 ∈ (𝑔 NeighbVtx 𝑣)
17	16, 7, 13	crab 3068	. . 3 class {𝑣 ∈ (Vtx‘𝑔) ∣ ∀𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣})𝑛 ∈ (𝑔 NeighbVtx 𝑣)}
18	2, 3, 17	cmpt 5157	. 2 class (𝑔 ∈ V ↦ {𝑣 ∈ (Vtx‘𝑔) ∣ ∀𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣})𝑛 ∈ (𝑔 NeighbVtx 𝑣)})
19	1, 18	wceq 1539	1 wff UnivVtx = (𝑔 ∈ V ↦ {𝑣 ∈ (Vtx‘𝑔) ∣ ∀𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣})𝑛 ∈ (𝑔 NeighbVtx 𝑣)})

This definition is referenced by:  uvtxval  27754