This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem edgov

Description: The edges of a graph represented as ordered pair, shown as operation value. Although a little less intuitive, this representation is often used because it is shorter than the representation as function value of a graph given as ordered pair, see edgopval . The representation ran E for the set of edges is even shorter, though. (Contributed by AV, 2-Jan-2020) (Revised by AV, 13-Oct-2020)

		Ref	Expression
	Assertion	edgov	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋 ) → ( 𝑉 Edg 𝐸 ) = ran 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		df-ov	⊢ ( 𝑉 Edg 𝐸 ) = ( Edg ‘ ⟨ 𝑉 , 𝐸 ⟩ )
2		edgopval	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋 ) → ( Edg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = ran 𝐸 )
3	1 2	eqtrid	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋 ) → ( 𝑉 Edg 𝐸 ) = ran 𝐸 )