Definition df-uvtx 29544

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 29543	. 2 class UnivVtx
2		vg	. . 3 setvar 𝑔
3		cvv 3453	. . 3 class V
4		vn	. . . . . . 7 setvar 𝑛
5	4	cv 1558	. . . . . 6 class 𝑛
6	2	cv 1558	. . . . . . 7 class 𝑔
7		vv	. . . . . . . 8 setvar 𝑣
8	7	cv 1558	. . . . . . 7 class 𝑣
9		cnbgr 29490	. . . . . . 7 class NeighbVtx
10	6, 8, 9	co 7391	. . . . . 6 class (𝑔 NeighbVtx 𝑣)
11	5, 10	wcel 2141	. . . . 5 wff 𝑛 ∈ (𝑔 NeighbVtx 𝑣)
12		cvtx 29154	. . . . . . 7 class Vtx
13	6, 12	cfv 6516	. . . . . 6 class (Vtx‘𝑔)
14	8	csn 4579	. . . . . 6 class {𝑣}
15	13, 14	cdif 3899	. . . . 5 class ((Vtx‘𝑔) ∖ {𝑣})
16	11, 4, 15	wral 3075	. . . 4 wff ∀𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣})𝑛 ∈ (𝑔 NeighbVtx 𝑣)
17	16, 7, 13	crab 3413	. . 3 class {𝑣 ∈ (Vtx‘𝑔) ∣ ∀𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣})𝑛 ∈ (𝑔 NeighbVtx 𝑣)}
18	2, 3, 17	cmpt 5178	. 2 class (𝑔 ∈ V ↦ {𝑣 ∈ (Vtx‘𝑔) ∣ ∀𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣})𝑛 ∈ (𝑔 NeighbVtx 𝑣)})
19	1, 18	wceq 1559	1 wff UnivVtx = (𝑔 ∈ V ↦ {𝑣 ∈ (Vtx‘𝑔) ∣ ∀𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣})𝑛 ∈ (𝑔 NeighbVtx 𝑣)})

This definition is referenced by:  uvtxval  29545