Theorem opvtxov

Description: The set of vertices 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	opvtxov	$$⊢\left(V\in X\wedge E\in Y\right)\to V\mathrm{Vtx}E=V$$

Proof

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