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	$$⊢\left(V\in W\wedge E\in X\right)\to V\mathrm{Edg}E=\mathrm{ran}E$$

Proof

Step	Hyp	Ref	Expression
1		df-ov	$$⊢V\mathrm{Edg}E=\mathrm{Edg}\left(⟨V,E⟩\right)$$
2		edgopval	$$⊢\left(V\in W\wedge E\in X\right)\to \mathrm{Edg}\left(⟨V,E⟩\right)=\mathrm{ran}E$$
3	1 2	syl5eq	$$⊢\left(V\in W\wedge E\in X\right)\to V\mathrm{Edg}E=\mathrm{ran}E$$