Description: The set of vertices of a graph represented as an ordered pair of vertices and indexed edges. (Contributed by AV, 9-Jan-2020) (Revised by AV, 21-Sep-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | opvtxval | ⊢ ( 𝐺 ∈ ( V × V ) → ( Vtx ‘ 𝐺 ) = ( 1st ‘ 𝐺 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vtxval | ⊢ ( Vtx ‘ 𝐺 ) = if ( 𝐺 ∈ ( V × V ) , ( 1st ‘ 𝐺 ) , ( Base ‘ 𝐺 ) ) | |
2 | iftrue | ⊢ ( 𝐺 ∈ ( V × V ) → if ( 𝐺 ∈ ( V × V ) , ( 1st ‘ 𝐺 ) , ( Base ‘ 𝐺 ) ) = ( 1st ‘ 𝐺 ) ) | |
3 | 1 2 | syl5eq | ⊢ ( 𝐺 ∈ ( V × V ) → ( Vtx ‘ 𝐺 ) = ( 1st ‘ 𝐺 ) ) |