Metamath Proof Explorer

Theorem opiedgfv

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, 21-Sep-2020)

		Ref	Expression
	Assertion	opiedgfv	$⊢ (V \in X \land E \in Y) \to iEdg (⟨V, E⟩) = E$

Proof

Step	Hyp	Ref	Expression
1		opelvvg	$⊢ (V \in X \land E \in Y) \to ⟨V, E⟩ \in (V \times V)$
2		opiedgval	$⊢ ⟨V, E⟩ \in (V \times V) \to iEdg (⟨V, E⟩) = 2^{nd} (⟨V, E⟩)$
3	1 2	syl	$⊢ (V \in X \land E \in Y) \to iEdg (⟨V, E⟩) = 2^{nd} (⟨V, E⟩)$
4		op2ndg	$⊢ (V \in X \land E \in Y) \to 2^{nd} (⟨V, E⟩) = E$
5	3 4	eqtrd	$⊢ (V \in X \land E \in Y) \to iEdg (⟨V, E⟩) = E$