Theorem opiedgov

Description: The set of indexed edges of a graph represented as an ordered pair of vertices and indexed edges as operation value. (Contributed by AV, 21-Sep-2020)

	Ref	Expression
Assertion	opiedgov	$$⊢\left(V\in X\wedge E\in Y\right)\to V\mathrm{iEdg}E=E$$

Proof

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