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

Definition df-nbgra 23347
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  =  ( g  e.  _V , 
k  e.  ( 1st `  g )  |->  { n  e.  ( 1st `  g
)  |  { k ,  n }  e.  ran  ( 2nd `  g
) } )
Distinct variable group:    g, k, n

Detailed syntax breakdown of Definition df-nbgra
StepHypRef Expression
1 cnbgra 23344 . 2  class Neighbors
2 vg . . 3  setvar  g
3 vk . . 3  setvar  k
4 cvv 2987 . . 3  class  _V
52cv 1368 . . . 4  class  g
6 c1st 6590 . . . 4  class  1st
75, 6cfv 5433 . . 3  class  ( 1st `  g )
83cv 1368 . . . . . 6  class  k
9 vn . . . . . . 7  setvar  n
109cv 1368 . . . . . 6  class  n
118, 10cpr 3894 . . . . 5  class  { k ,  n }
12 c2nd 6591 . . . . . . 7  class  2nd
135, 12cfv 5433 . . . . . 6  class  ( 2nd `  g )
1413crn 4856 . . . . 5  class  ran  ( 2nd `  g )
1511, 14wcel 1756 . . . 4  wff  { k ,  n }  e.  ran  ( 2nd `  g
)
1615, 9, 7crab 2734 . . 3  class  { n  e.  ( 1st `  g
)  |  { k ,  n }  e.  ran  ( 2nd `  g
) }
172, 3, 4, 7, 16cmpt2 6108 . 2  class  ( g  e.  _V ,  k  e.  ( 1st `  g
)  |->  { n  e.  ( 1st `  g
)  |  { k ,  n }  e.  ran  ( 2nd `  g
) } )
181, 17wceq 1369 1  wff Neighbors  =  ( g  e.  _V , 
k  e.  ( 1st `  g )  |->  { n  e.  ( 1st `  g
)  |  { k ,  n }  e.  ran  ( 2nd `  g
) } )
Colors of variables: wff setvar class
This definition is referenced by:  nbgraop  23350  nbgrael  23352  nbgranv0  23353
  Copyright terms: Public domain W3C validator