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	⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		fveqeq2	⊢ ( 𝑤 = 𝑊 → ( ( ♯ ‘ 𝑤 ) = 𝑁 ↔ ( ♯ ‘ 𝑊 ) = 𝑁 ) )
2		clwwlkn	⊢ ( 𝑁 ClWWalksN 𝐺 ) = { 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑁 }
3	1 2	elrab2	⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) )