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

Definition df-nbgra 25090
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 25087 . 2  class Neighbors
2 vg . . 3  setvar  g
3 vk . . 3  setvar  k
4 cvv 3022 . . 3  class  _V
52cv 1436 . . . 4  class  g
6 c1st 6749 . . . 4  class  1st
75, 6cfv 5544 . . 3  class  ( 1st `  g )
83cv 1436 . . . . . 6  class  k
9 vn . . . . . . 7  setvar  n
109cv 1436 . . . . . 6  class  n
118, 10cpr 3943 . . . . 5  class  { k ,  n }
12 c2nd 6750 . . . . . . 7  class  2nd
135, 12cfv 5544 . . . . . 6  class  ( 2nd `  g )
1413crn 4797 . . . . 5  class  ran  ( 2nd `  g )
1511, 14wcel 1872 . . . 4  wff  { k ,  n }  e.  ran  ( 2nd `  g
)
1615, 9, 7crab 2718 . . 3  class  { n  e.  ( 1st `  g
)  |  { k ,  n }  e.  ran  ( 2nd `  g
) }
172, 3, 4, 7, 16cmpt2 6251 . 2  class  ( g  e.  _V ,  k  e.  ( 1st `  g
)  |->  { n  e.  ( 1st `  g
)  |  { k ,  n }  e.  ran  ( 2nd `  g
) } )
181, 17wceq 1437 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  25093  nbgraopALT  25094  nbgrael  25096  nbgranv0  25097
  Copyright terms: Public domain W3C validator