Metamath Proof Explorer


Theorem opiedgfvi

Description: The set of indexed edges 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
opvtxfvi.e 𝐸 ∈ V
Assertion opiedgfvi ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸

Proof

Step Hyp Ref Expression
1 opvtxfvi.v 𝑉 ∈ V
2 opvtxfvi.e 𝐸 ∈ V
3 opiedgfv ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) → ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 )
4 1 2 3 mp2an ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸