Metamath Proof Explorer


Theorem funvtxval

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 FunGBasendxefndxdomGVtxG=BaseG

Proof

Step Hyp Ref Expression
1 basendxnedgfndx Basendxefndx
2 fvex BasendxV
3 fvex efndxV
4 2 3 funvtxdm2val FunGBasendxefndxBasendxefndxdomGVtxG=BaseG
5 1 4 mp3an2 FunGBasendxefndxdomGVtxG=BaseG