Metamath Proof Explorer

Theorem opiedgval

Description: The set of indexed edges of a graph represented as an ordered pair of vertices and indexed edges. (Contributed by AV, 21-Sep-2020)

		Ref	Expression
	Assertion	opiedgval	\|- ( G e. ( _V X. _V ) -> ( iEdg ` G ) = ( 2nd ` G ) )

Step	Hyp	Ref	Expression
1		iedgval	\|- ( iEdg ` G ) = if ( G e. ( _V X. _V ) , ( 2nd ` G ) , ( .ef ` G ) )
2		iftrue	\|- ( G e. ( _V X. _V ) -> if ( G e. ( _V X. _V ) , ( 2nd ` G ) , ( .ef ` G ) ) = ( 2nd ` G ) )
3	1 2	syl5eq	\|- ( G e. ( _V X. _V ) -> ( iEdg ` G ) = ( 2nd ` G ) )

Step

Hyp

Ref

Expression

 |-  ( iEdg ` G ) = if ( G e. ( _V X. _V ) , ( 2nd ` G ) , ( .ef ` G ) )

 |-  ( G e. ( _V X. _V ) -> if ( G e. ( _V X. _V ) , ( 2nd ` G ) , ( .ef ` G ) ) = ( 2nd ` G ) )

1 2

 |-  ( G e. ( _V X. _V ) -> ( iEdg ` G ) = ( 2nd ` G ) )