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

Metamath Proof Explorer

Theorem wlkop

Description: A walk is an ordered pair. (Contributed by Alexander van der Vekens, 30-Jun-2018) (Revised by AV, 1-Jan-2021)

		Ref	Expression
	Assertion	wlkop	$⊢ W \in Walks (G) \to W = ⟨1^{st} (W), 2^{nd} (W)⟩$

Step	Hyp	Ref	Expression
1		relwlk	$⊢ Rel Walks (G)$
2		1st2nd	$⊢ (Rel Walks (G) \land W \in Walks (G)) \to W = ⟨1^{st} (W), 2^{nd} (W)⟩$
3	1 2	mpan	$⊢ W \in Walks (G) \to W = ⟨1^{st} (W), 2^{nd} (W)⟩$