Theorem edgopval

Description: The edges of a graph represented as ordered pair. (Contributed by AV, 1-Jan-2020) (Revised by AV, 13-Oct-2020)

	Ref	Expression
Assertion	edgopval	$$⊢\left(V\in W\wedge E\in X\right)\to \mathrm{Edg}\left(⟨V,E⟩\right)=\mathrm{ran}E$$

Proof

Step	Hyp	Ref	Expression
1		edgval	$$⊢\mathrm{Edg}\left(⟨V,E⟩\right)=\mathrm{ran}\mathrm{iEdg}\left(⟨V,E⟩\right)$$
2		opiedgfv	$$⊢\left(V\in W\wedge E\in X\right)\to \mathrm{iEdg}\left(⟨V,E⟩\right)=E$$
3	2	rneqd	$$⊢\left(V\in W\wedge E\in X\right)\to \mathrm{ran}\mathrm{iEdg}\left(⟨V,E⟩\right)=\mathrm{ran}E$$
4	1 3	syl5eq	$$⊢\left(V\in W\wedge E\in X\right)\to \mathrm{Edg}\left(⟨V,E⟩\right)=\mathrm{ran}E$$