Definition df-nbgr 26228

Description: Define the (open) neighborhood resp. the class of all neighbors of a vertex (in a graph), see definition in section I.1 of [Bollobas] p. 3 or definition in section 1.1 of [Diestel] p. 3. The neighborhood/neighbors of a vertex are all (other) vertices which are connected with this vertex by an edge. In contrast to a closed neighborhood, a vertex is not a neighbor of itself. This definition is applicable even for arbitrary hypergraphs.

Remark: To distinguish this definition from other definitions for neighborhoods resp. neighbors (e.g., nei in Topology, see df-nei 20902), the suffix Vtx is added to the class constant NeighbVtx. (Contributed by Alexander van der Vekens and Mario Carneiro, 7-Oct-2017.) (Revised by AV, 24-Oct-2020.)

Assertion

Ref	Expression
df-nbgr	|- NeighbVtx = ( g e. _V , v e. (Vtx ` g ) |-> { n e. ( (Vtx ` g ) \ { v } ) | E. e e. (Edg ` g ) { v , n } C_ e } )

Distinct variable group:   e, g, n, v

Detailed syntax breakdown of Definition df-nbgr

Step	Hyp	Ref	Expression
1		cnbgr 26224	. 2 class NeighbVtx
2		vg	. . 3 setvar g
3		vv	. . 3 setvar v
4		cvv 3200	. . 3 class _V
5	2	cv 1482	. . . 4 class g
6		cvtx 25874	. . . 4 class Vtx
7	5, 6	cfv 5888	. . 3 class (Vtx ` g )
8	3	cv 1482	. . . . . . 7 class v
9		vn	. . . . . . . 8 setvar n
10	9	cv 1482	. . . . . . 7 class n
11	8, 10	cpr 4179	. . . . . 6 class { v , n }
12		ve	. . . . . . 7 setvar e
13	12	cv 1482	. . . . . 6 class e
14	11, 13	wss 3574	. . . . 5 wff { v , n } C_ e
15		cedg 25939	. . . . . 6 class Edg
16	5, 15	cfv 5888	. . . . 5 class (Edg ` g )
17	14, 12, 16	wrex 2913	. . . 4 wff E. e e. (Edg ` g ) { v , n } C_ e
18	8	csn 4177	. . . . 5 class { v }
19	7, 18	cdif 3571	. . . 4 class ( (Vtx ` g ) \ { v } )
20	17, 9, 19	crab 2916	. . 3 class { n e. ( (Vtx ` g ) \ { v } ) | E. e e. (Edg ` g ) { v , n } C_ e }
21	2, 3, 4, 7, 20	cmpt2 6652	. 2 class ( g e. _V , v e. (Vtx ` g ) |-> { n e. ( (Vtx ` g ) \ { v } ) | E. e e. (Edg ` g ) { v , n } C_ e } )
22	1, 21	wceq 1483	1 wff NeighbVtx = ( g e. _V , v e. (Vtx ` g ) |-> { n e. ( (Vtx ` g ) \ { v } ) | E. e e. (Edg ` g ) { v , n } C_ e } )

This definition is referenced by:  nbgrprc0  26229  nbgrcl  26233  nbgrval  26234  nbgrnvtx0  26237