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

Definition df-nbgra 25715
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 25712 . 2 class Neighbors
2 vg . . 3 setvar 𝑔
3 vk . . 3 setvar 𝑘
4 cvv 3172 . . 3 class V
52cv 1473 . . . 4 class 𝑔
6 c1st 7034 . . . 4 class 1st
75, 6cfv 5790 . . 3 class (1st𝑔)
83cv 1473 . . . . . 6 class 𝑘
9 vn . . . . . . 7 setvar 𝑛
109cv 1473 . . . . . 6 class 𝑛
118, 10cpr 4126 . . . . 5 class {𝑘, 𝑛}
12 c2nd 7035 . . . . . . 7 class 2nd
135, 12cfv 5790 . . . . . 6 class (2nd𝑔)
1413crn 5029 . . . . 5 class ran (2nd𝑔)
1511, 14wcel 1976 . . . 4 wff {𝑘, 𝑛} ∈ ran (2nd𝑔)
1615, 9, 7crab 2899 . . 3 class {𝑛 ∈ (1st𝑔) ∣ {𝑘, 𝑛} ∈ ran (2nd𝑔)}
172, 3, 4, 7, 16cmpt2 6529 . 2 class (𝑔 ∈ V, 𝑘 ∈ (1st𝑔) ↦ {𝑛 ∈ (1st𝑔) ∣ {𝑘, 𝑛} ∈ ran (2nd𝑔)})
181, 17wceq 1474 1 wff Neighbors = (𝑔 ∈ V, 𝑘 ∈ (1st𝑔) ↦ {𝑛 ∈ (1st𝑔) ∣ {𝑘, 𝑛} ∈ ran (2nd𝑔)})
Colors of variables: wff setvar class
This definition is referenced by:  nbgraop  25718  nbgraopALT  25719  nbgrael  25721  nbgranv0  25722
  Copyright terms: Public domain W3C validator