Metamath Proof Explorer


Theorem erclwwlkrel

Description: .~ is a relation. (Contributed by Alexander van der Vekens, 25-Mar-2018) (Revised by AV, 29-Apr-2021)

Ref Expression
Hypothesis erclwwlk.r ˙ = u w | u ClWWalks G w ClWWalks G n 0 w u = w cyclShift n
Assertion erclwwlkrel Rel ˙

Proof

Step Hyp Ref Expression
1 erclwwlk.r ˙ = u w | u ClWWalks G w ClWWalks G n 0 w u = w cyclShift n
2 1 relopabi Rel ˙