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

Metamath Proof Explorer

Theorem isclwwlkn

Description: A word over the set of vertices representing a closed walk of a fixed length. (Contributed by Alexander van der Vekens, 15-Mar-2018) (Revised by AV, 24-Apr-2021) (Revised by AV, 22-Mar-2022)

Ref Expression
Assertion isclwwlkn ⊢ W ∈ N ClWWalksN G ↔ W ∈ ClWWalks ⁡ G ∧ W = N

Proof

Step Hyp Ref Expression
1 fveqeq2 ⊢ w = W → w = N ↔ W = N
2 clwwlkn ⊢ N ClWWalksN G = w ∈ ClWWalks ⁡ G | w = N
3 1 2 elrab2 ⊢ W ∈ N ClWWalksN G ↔ W ∈ ClWWalks ⁡ G ∧ W = N