Definition df-uvtx 26691

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 26690	. 2 class UnivVtx
2		vg	. . 3 setvar 𝑔
3		cvv 3414	. . 3 class V
4		vn	. . . . . . 7 setvar 𝑛
5	4	cv 1655	. . . . . 6 class 𝑛
6	2	cv 1655	. . . . . . 7 class 𝑔
7		vv	. . . . . . . 8 setvar 𝑣
8	7	cv 1655	. . . . . . 7 class 𝑣
9		cnbgr 26636	. . . . . . 7 class NeighbVtx
10	6, 8, 9	co 6910	. . . . . 6 class (𝑔 NeighbVtx 𝑣)
11	5, 10	wcel 2164	. . . . 5 wff 𝑛 ∈ (𝑔 NeighbVtx 𝑣)
12		cvtx 26301	. . . . . . 7 class Vtx
13	6, 12	cfv 6127	. . . . . 6 class (Vtx‘𝑔)
14	8	csn 4399	. . . . . 6 class {𝑣}
15	13, 14	cdif 3795	. . . . 5 class ((Vtx‘𝑔) ∖ {𝑣})
16	11, 4, 15	wral 3117	. . . 4 wff ∀𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣})𝑛 ∈ (𝑔 NeighbVtx 𝑣)
17	16, 7, 13	crab 3121	. . 3 class {𝑣 ∈ (Vtx‘𝑔) ∣ ∀𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣})𝑛 ∈ (𝑔 NeighbVtx 𝑣)}
18	2, 3, 17	cmpt 4954	. 2 class (𝑔 ∈ V ↦ {𝑣 ∈ (Vtx‘𝑔) ∣ ∀𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣})𝑛 ∈ (𝑔 NeighbVtx 𝑣)})
19	1, 18	wceq 1656	1 wff UnivVtx = (𝑔 ∈ V ↦ {𝑣 ∈ (Vtx‘𝑔) ∣ ∀𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣})𝑛 ∈ (𝑔 NeighbVtx 𝑣)})

This definition is referenced by:  uvtxval  26692