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
|- ( G e. ( _V X. _V ) -> ( Vtx ` G ) = ( 1st ` G ) )

Proof

Step Hyp Ref Expression
1 vtxval
 |-  ( Vtx ` G ) = if ( G e. ( _V X. _V ) , ( 1st ` G ) , ( Base ` G ) )
2 iftrue
 |-  ( G e. ( _V X. _V ) -> if ( G e. ( _V X. _V ) , ( 1st ` G ) , ( Base ` G ) ) = ( 1st ` G ) )
3 1 2 syl5eq
 |-  ( G e. ( _V X. _V ) -> ( Vtx ` G ) = ( 1st ` G ) )