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	⊢ ( 𝐺 ∈ ( V × V ) → ( iEdg ‘ 𝐺 ) = ( 2nd ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		iedgval	⊢ ( iEdg ‘ 𝐺 ) = if ( 𝐺 ∈ ( V × V ) , ( 2nd ‘ 𝐺 ) , ( .ef ‘ 𝐺 ) )
2		iftrue	⊢ ( 𝐺 ∈ ( V × V ) → if ( 𝐺 ∈ ( V × V ) , ( 2nd ‘ 𝐺 ) , ( .ef ‘ 𝐺 ) ) = ( 2nd ‘ 𝐺 ) )
3	1 2	syl5eq	⊢ ( 𝐺 ∈ ( V × V ) → ( iEdg ‘ 𝐺 ) = ( 2nd ‘ 𝐺 ) )