Description: The edges of a graph represented as ordered pair. (Contributed by AV, 1-Jan-2020) (Revised by AV, 13-Oct-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | edgopval | ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋 ) → ( Edg ‘ 〈 𝑉 , 𝐸 〉 ) = ran 𝐸 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | edgval | ⊢ ( Edg ‘ 〈 𝑉 , 𝐸 〉 ) = ran ( iEdg ‘ 〈 𝑉 , 𝐸 〉 ) | |
2 | opiedgfv | ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋 ) → ( iEdg ‘ 〈 𝑉 , 𝐸 〉 ) = 𝐸 ) | |
3 | 2 | rneqd | ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋 ) → ran ( iEdg ‘ 〈 𝑉 , 𝐸 〉 ) = ran 𝐸 ) |
4 | 1 3 | eqtrid | ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋 ) → ( Edg ‘ 〈 𝑉 , 𝐸 〉 ) = ran 𝐸 ) |