Metamath Proof Explorer


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 V X E Y V Vtx E = V

Proof

Step Hyp Ref Expression
1 df-ov V Vtx E = Vtx V E
2 opvtxfv V X E Y Vtx V E = V
3 1 2 syl5eq V X E Y V Vtx E = V