Theorem edgopval

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 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		edgval	⊢ ( Edg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = ran ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ )
2		opiedgfv	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋 ) → ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 )
3	2	rneqd	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋 ) → ran ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = ran 𝐸 )
4	1 3	syl5eq	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋 ) → ( Edg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = ran 𝐸 )