Metamath Proof Explorer


Theorem opvtxval

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𝐺 ) )

Proof

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𝐺 ) )