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 e. ( Walks ` G ) -> W = <. ( 1st ` W ) , ( 2nd ` W ) >. )

Proof

Step Hyp Ref Expression
1 relwlk 
 |-  Rel ( Walks ` G )
2 1st2nd 
 |-  ( ( Rel ( Walks ` G ) /\ W e. ( Walks ` G ) ) -> W = <. ( 1st ` W ) , ( 2nd ` W ) >. )
3 1 2 mpan 
 |-  ( W e. ( Walks ` G ) -> W = <. ( 1st ` W ) , ( 2nd ` W ) >. )