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\in \left(N\mathrm{ClWWalksN}G\right)\leftrightarrow \left(W\in \mathrm{ClWWalks}\left(G\right)\wedge \left|W\right|=N\right)$$

Proof

Step	Hyp	Ref	Expression
1		fveqeq2	$$⊢w=W\to \left(\left|w\right|=N\leftrightarrow \left|W\right|=N\right)$$
2		clwwlkn	$$⊢N\mathrm{ClWWalksN}G=\left\{w\in \mathrm{ClWWalks}\left(G\right)|\left|w\right|=N\right\}$$
3	1 2	elrab2	$$⊢W\in \left(N\mathrm{ClWWalksN}G\right)\leftrightarrow \left(W\in \mathrm{ClWWalks}\left(G\right)\wedge \left|W\right|=N\right)$$