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

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
StepHypRef Expression
1 cnbgra 25946 . 2 class Neighbors
2 vg . . 3 setvar 𝑔
3 vk . . 3 setvar 𝑘
4 cvv 3173 . . 3 class V
52cv 1474 . . . 4 class 𝑔
6 c1st 7057 . . . 4 class 1st
75, 6cfv 5804 . . 3 class (1st𝑔)
83cv 1474 . . . . . 6 class 𝑘
9 vn . . . . . . 7 setvar 𝑛
109cv 1474 . . . . . 6 class 𝑛
118, 10cpr 4127 . . . . 5 class {𝑘, 𝑛}
12 c2nd 7058 . . . . . . 7 class 2nd
135, 12cfv 5804 . . . . . 6 class (2nd𝑔)
1413crn 5039 . . . . 5 class ran (2nd𝑔)
1511, 14wcel 1977 . . . 4 wff {𝑘, 𝑛} ∈ ran (2nd𝑔)
1615, 9, 7crab 2900 . . 3 class {𝑛 ∈ (1st𝑔) ∣ {𝑘, 𝑛} ∈ ran (2nd𝑔)}
172, 3, 4, 7, 16cmpt2 6551 . 2 class (𝑔 ∈ V, 𝑘 ∈ (1st𝑔) ↦ {𝑛 ∈ (1st𝑔) ∣ {𝑘, 𝑛} ∈ ran (2nd𝑔)})
181, 17wceq 1475 1 wff Neighbors = (𝑔 ∈ V, 𝑘 ∈ (1st𝑔) ↦ {𝑛 ∈ (1st𝑔) ∣ {𝑘, 𝑛} ∈ ran (2nd𝑔)})
 Colors of variables: wff setvar class This definition is referenced by:  nbgraop  25952  nbgraopALT  25953  nbgrael  25955  nbgranv0  25956
 Copyright terms: Public domain W3C validator