Description: The set of vertices of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 22-Sep-2020) (Revised by AV, 7-Jun-2021) (Revised by AV, 12-Nov-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | funvtxval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | basendxnedgfndx | |
|
2 | fvex | |
|
3 | fvex | |
|
4 | 2 3 | funvtxdm2val | |
5 | 1 4 | mp3an2 | |