Metamath Proof Explorer

Theorem nbusgrvtx

Description: The set of neighbors of a vertex in a simple graph. (Contributed by Alexander van der Vekens, 9-Oct-2017) (Revised by AV, 26-Oct-2020) (Proof shortened by AV, 27-Nov-2020)

Ref Expression
Hypotheses nbuhgr.v ⊢ V = Vtx ⁡ G
nbuhgr.e ⊢ E = Edg ⁡ G
Assertion nbusgrvtx ⊢ G ∈ USGraph ∧ N ∈ V → G NeighbVtx N = n ∈ V | N n ∈ E

Proof

Step Hyp Ref Expression
1 nbuhgr.v ⊢ V = Vtx ⁡ G
2 nbuhgr.e ⊢ E = Edg ⁡ G
3 usgrumgr ⊢ G ∈ USGraph → G ∈ UMGraph
4 1 2 nbumgrvtx ⊢ G ∈ UMGraph ∧ N ∈ V → G NeighbVtx N = n ∈ V | N n ∈ E
5 3 4 sylan ⊢ G ∈ USGraph ∧ N ∈ V → G NeighbVtx N = n ∈ V | N n ∈ E