Metamath Proof Explorer

Theorem opvtxfv

Description: The set of vertices 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	opvtxfv	$⊢ (V \in X \land E \in Y) \to Vtx (⟨V, E⟩) = V$

Proof

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