This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database GRAPH THEORY Vertices and edges Vertices and indexed edges The vertices and edges of a graph represented as ordered pair opvtxfvi
Description: The set of vertices of a graph represented as an ordered pair of
vertices and indexed edges as function value. (Contributed by AV , 4-Mar-2021)
Ref
Expression
Hypotheses
opvtxfvi.v ⊢ V ∈ V
opvtxfvi.e ⊢ E ∈ V
Assertion
opvtxfvi ⊢ Vtx V E = V
Proof
Step
Hyp
Ref
Expression
1
opvtxfvi.v ⊢ V ∈ V
2
opvtxfvi.e ⊢ E ∈ V
3
opvtxfv ⊢ V ∈ V ∧ E ∈ V → Vtx V E = V
4
1 2 3
mp2an ⊢ Vtx V E = V