Definition df-uvtxa 26230

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) resp. 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-uvtxa	⊢ UnivVtx = (𝑔 ∈ V ↦ {𝑣 ∈ (Vtx‘𝑔) ∣ ∀𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣})𝑛 ∈ (𝑔 NeighbVtx 𝑣)})

Distinct variable group:   𝑣,𝑔,𝑛

Detailed syntax breakdown of Definition df-uvtxa

Step	Hyp	Ref	Expression
1		cuvtxa 26225	. 2 class UnivVtx
2		vg	. . 3 setvar 𝑔
3		cvv 3200	. . 3 class V
4		vn	. . . . . . 7 setvar 𝑛
5	4	cv 1482	. . . . . 6 class 𝑛
6	2	cv 1482	. . . . . . 7 class 𝑔
7		vv	. . . . . . . 8 setvar 𝑣
8	7	cv 1482	. . . . . . 7 class 𝑣
9		cnbgr 26224	. . . . . . 7 class NeighbVtx
10	6, 8, 9	co 6650	. . . . . 6 class (𝑔 NeighbVtx 𝑣)
11	5, 10	wcel 1990	. . . . 5 wff 𝑛 ∈ (𝑔 NeighbVtx 𝑣)
12		cvtx 25874	. . . . . . 7 class Vtx
13	6, 12	cfv 5888	. . . . . 6 class (Vtx‘𝑔)
14	8	csn 4177	. . . . . 6 class {𝑣}
15	13, 14	cdif 3571	. . . . 5 class ((Vtx‘𝑔) ∖ {𝑣})
16	11, 4, 15	wral 2912	. . . 4 wff ∀𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣})𝑛 ∈ (𝑔 NeighbVtx 𝑣)
17	16, 7, 13	crab 2916	. . 3 class {𝑣 ∈ (Vtx‘𝑔) ∣ ∀𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣})𝑛 ∈ (𝑔 NeighbVtx 𝑣)}
18	2, 3, 17	cmpt 4729	. 2 class (𝑔 ∈ V ↦ {𝑣 ∈ (Vtx‘𝑔) ∣ ∀𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣})𝑛 ∈ (𝑔 NeighbVtx 𝑣)})
19	1, 18	wceq 1483	1 wff UnivVtx = (𝑔 ∈ V ↦ {𝑣 ∈ (Vtx‘𝑔) ∣ ∀𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣})𝑛 ∈ (𝑔 NeighbVtx 𝑣)})

This definition is referenced by:  uvtxaval  26287