This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ V × V → iEdg ⁡ G = 2 nd ⁡ G

Proof

Step Hyp Ref Expression
1 iedgval ⊢ iEdg ⁡ G = if G ∈ V × V 2 nd ⁡ G ef ⁡ G
2 iftrue ⊢ G ∈ V × V → if G ∈ V × V 2 nd ⁡ G ef ⁡ G = 2 nd ⁡ G
3 1 2 eqtrid ⊢ G ∈ V × V → iEdg ⁡ G = 2 nd ⁡ G