Metamath Proof Explorer

Theorem isclwwlknon

Description: A word over the set of vertices representing a closed walk on vertex X of length N in a graph G . (Contributed by AV, 25-Feb-2022) (Revised by AV, 24-Mar-2022)

Ref Expression
Assertion isclwwlknon ⊢ W ∈ X ClWWalksNOn ⁡ G N ↔ W ∈ N ClWWalksN G ∧ W ⁡ 0 = X

Proof

Step Hyp Ref Expression
1 fveq1 ⊢ w = W → w ⁡ 0 = W ⁡ 0
2 1 eqeq1d ⊢ w = W → w ⁡ 0 = X ↔ W ⁡ 0 = X
3 clwwlknon ⊢ X ClWWalksNOn ⁡ G N = w ∈ N ClWWalksN G | w ⁡ 0 = X
4 2 3 elrab2 ⊢ W ∈ X ClWWalksNOn ⁡ G N ↔ W ∈ N ClWWalksN G ∧ W ⁡ 0 = X