Metamath Proof Explorer


Theorem nbusgrf1o

Description: The set of neighbors of a vertex is isomorphic to the set of edges containing the vertex in a simple graph. (Contributed by Alexander van der Vekens, 19-Dec-2017) (Revised by AV, 28-Oct-2020)

Ref Expression
Hypotheses nbusgrf1o.v V = Vtx G
nbusgrf1o.e E = Edg G
Assertion nbusgrf1o G USGraph U V f f : G NeighbVtx U 1-1 onto e E | U e

Proof

Step Hyp Ref Expression
1 nbusgrf1o.v V = Vtx G
2 nbusgrf1o.e E = Edg G
3 eqid G NeighbVtx U = G NeighbVtx U
4 eleq2w e = c U e U c
5 4 cbvrabv e E | U e = c E | U c
6 1 2 3 5 nbusgrf1o1 G USGraph U V f f : G NeighbVtx U 1-1 onto e E | U e