Description: The set of vertices of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 23-Sep-2020)
Ref | Expression | ||
---|---|---|---|
Hypothesis | struct2grvtx.g | ||
Assertion | struct2grvtx |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | struct2grvtx.g | ||
2 | edgfndxnn | ||
3 | baseltedgf | ||
4 | 2 3 1 | structvtxval |