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

Step

Hyp

Ref

Expression

vtxval

 |-  ( Vtx ` G ) = if ( G e. ( _V X. _V ) , ( 1st ` G ) , ( Base ` G ) )

iftrue

 |-  ( G e. ( _V X. _V ) -> if ( G e. ( _V X. _V ) , ( 1st ` G ) , ( Base ` G ) ) = ( 1st ` G ) )

1 2

eqtrid

 |-  ( G e. ( _V X. _V ) -> ( Vtx ` G ) = ( 1st ` G ) )