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 ‘ 〈 𝑉 , 𝐸 〉 ) = 𝐸 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opvtxfvi.v | ⊢ 𝑉 ∈ V | |
2 | opvtxfvi.e | ⊢ 𝐸 ∈ V | |
3 | opiedgfv | ⊢ ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) → ( iEdg ‘ 〈 𝑉 , 𝐸 〉 ) = 𝐸 ) | |
4 | 1 2 3 | mp2an | ⊢ ( iEdg ‘ 〈 𝑉 , 𝐸 〉 ) = 𝐸 |