Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-nbgra Structured version   Unicode version

Definition df-nbgra 24243
 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
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-nbgra
StepHypRef Expression
1 cnbgra 24240 . 2 Neighbors
2 vg . . 3
3 vk . . 3
4 cvv 3118 . . 3
52cv 1378 . . . 4
6 c1st 6793 . . . 4
75, 6cfv 5594 . . 3
83cv 1378 . . . . . 6
9 vn . . . . . . 7
109cv 1378 . . . . . 6
118, 10cpr 4035 . . . . 5
12 c2nd 6794 . . . . . . 7
135, 12cfv 5594 . . . . . 6
1413crn 5006 . . . . 5
1511, 14wcel 1767 . . . 4
1615, 9, 7crab 2821 . . 3
172, 3, 4, 7, 16cmpt2 6297 . 2
181, 17wceq 1379 1 Neighbors
 Colors of variables: wff setvar class This definition is referenced by:  nbgraop  24246  nbgraopALT  24247  nbgrael  24249  nbgranv0  24250
 Copyright terms: Public domain W3C validator