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

Metamath Proof Explorer

Theorem edgov

Description: The edges of a graph represented as ordered pair, shown as operation value. Although a little less intuitive, this representation is often used because it is shorter than the representation as function value of a graph given as ordered pair, see edgopval . The representation ran E for the set of edges is even shorter, though. (Contributed by AV, 2-Jan-2020) (Revised by AV, 13-Oct-2020)

Ref Expression
Assertion edgov ⊢ V ∈ W ∧ E ∈ X → V Edg E = ran ⁡ E

Proof

Step Hyp Ref Expression
1 df-ov ⊢ V Edg E = Edg ⁡ V E
2 edgopval ⊢ V ∈ W ∧ E ∈ X → Edg ⁡ V E = ran ⁡ E
3 1 2 eqtrid ⊢ V ∈ W ∧ E ∈ X → V Edg E = ran ⁡ E