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 | ||
nbusgrf1o.e | |||
Assertion | nbusgrf1o |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nbusgrf1o.v | ||
2 | nbusgrf1o.e | ||
3 | eqid | ||
4 | eleq2w | ||
5 | 4 | cbvrabv | |
6 | 1 2 3 5 | nbusgrf1o1 |