Definition df-nbgra 25949

Description: Define the class of all Neighbors of a vertex in a graph. The neighbors of a vertex are all vertices which are connected with this vertex by an edge. (Contributed by Alexander van der Vekens and Mario Carneiro, 7-Oct-2017.)

Assertion

Ref	Expression
df-nbgra	⊢ Neighbors = (𝑔 ∈ V, 𝑘 ∈ (1st ‘𝑔) ↦ {𝑛 ∈ (1st ‘𝑔) ∣ {𝑘, 𝑛} ∈ ran (2nd ‘𝑔)})

Distinct variable group:   𝑔,𝑘,𝑛

Detailed syntax breakdown of Definition df-nbgra

Step	Hyp	Ref	Expression
1		cnbgra 25946	. 2 class Neighbors
2		vg	. . 3 setvar 𝑔
3		vk	. . 3 setvar 𝑘
4		cvv 3173	. . 3 class V
5	2	cv 1474	. . . 4 class 𝑔
6		c1st 7057	. . . 4 class 1st
7	5, 6	cfv 5804	. . 3 class (1st ‘𝑔)
8	3	cv 1474	. . . . . 6 class 𝑘
9		vn	. . . . . . 7 setvar 𝑛
10	9	cv 1474	. . . . . 6 class 𝑛
11	8, 10	cpr 4127	. . . . 5 class {𝑘, 𝑛}
12		c2nd 7058	. . . . . . 7 class 2nd
13	5, 12	cfv 5804	. . . . . 6 class (2nd ‘𝑔)
14	13	crn 5039	. . . . 5 class ran (2nd ‘𝑔)
15	11, 14	wcel 1977	. . . 4 wff {𝑘, 𝑛} ∈ ran (2nd ‘𝑔)
16	15, 9, 7	crab 2900	. . 3 class {𝑛 ∈ (1st ‘𝑔) ∣ {𝑘, 𝑛} ∈ ran (2nd ‘𝑔)}
17	2, 3, 4, 7, 16	cmpt2 6551	. 2 class (𝑔 ∈ V, 𝑘 ∈ (1st ‘𝑔) ↦ {𝑛 ∈ (1st ‘𝑔) ∣ {𝑘, 𝑛} ∈ ran (2nd ‘𝑔)})
18	1, 17	wceq 1475	1 wff Neighbors = (𝑔 ∈ V, 𝑘 ∈ (1st ‘𝑔) ↦ {𝑛 ∈ (1st ‘𝑔) ∣ {𝑘, 𝑛} ∈ ran (2nd ‘𝑔)})

This definition is referenced by:  nbgraop  25952  nbgraopALT  25953  nbgrael  25955  nbgranv0  25956