Definition df-uvtx 25951

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). (Contributed by Alexander van der Vekens, 12-Oct-2017.)

Assertion

Ref	Expression
df-uvtx	⊢ UnivVertex = (𝑣 ∈ V, 𝑒 ∈ V ↦ {𝑛 ∈ 𝑣 ∣ ∀𝑘 ∈ (𝑣 ∖ {𝑛}){𝑘, 𝑛} ∈ ran 𝑒})

Distinct variable group:   𝑣,𝑒,𝑘,𝑛

Detailed syntax breakdown of Definition df-uvtx

Step	Hyp	Ref	Expression
1		cuvtx 25948	. 2 class UnivVertex
2		vv	. . 3 setvar 𝑣
3		ve	. . 3 setvar 𝑒
4		cvv 3173	. . 3 class V
5		vk	. . . . . . . 8 setvar 𝑘
6	5	cv 1474	. . . . . . 7 class 𝑘
7		vn	. . . . . . . 8 setvar 𝑛
8	7	cv 1474	. . . . . . 7 class 𝑛
9	6, 8	cpr 4127	. . . . . 6 class {𝑘, 𝑛}
10	3	cv 1474	. . . . . . 7 class 𝑒
11	10	crn 5039	. . . . . 6 class ran 𝑒
12	9, 11	wcel 1977	. . . . 5 wff {𝑘, 𝑛} ∈ ran 𝑒
13	2	cv 1474	. . . . . 6 class 𝑣
14	8	csn 4125	. . . . . 6 class {𝑛}
15	13, 14	cdif 3537	. . . . 5 class (𝑣 ∖ {𝑛})
16	12, 5, 15	wral 2896	. . . 4 wff ∀𝑘 ∈ (𝑣 ∖ {𝑛}){𝑘, 𝑛} ∈ ran 𝑒
17	16, 7, 13	crab 2900	. . 3 class {𝑛 ∈ 𝑣 ∣ ∀𝑘 ∈ (𝑣 ∖ {𝑛}){𝑘, 𝑛} ∈ ran 𝑒}
18	2, 3, 4, 4, 17	cmpt2 6551	. 2 class (𝑣 ∈ V, 𝑒 ∈ V ↦ {𝑛 ∈ 𝑣 ∣ ∀𝑘 ∈ (𝑣 ∖ {𝑛}){𝑘, 𝑛} ∈ ran 𝑒})
19	1, 18	wceq 1475	1 wff UnivVertex = (𝑣 ∈ V, 𝑒 ∈ V ↦ {𝑛 ∈ 𝑣 ∣ ∀𝑘 ∈ (𝑣 ∖ {𝑛}){𝑘, 𝑛} ∈ ran 𝑒})

This definition is referenced by:  isuvtx  26016  uvtxisvtx  26018  uvtx0  26019  uvtx01vtx  26020