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 e. ( N ClWWalksN G ) <-> ( W e. ( ClWWalks ` G ) /\ ( # ` W ) = N ) )

Proof

Step	Hyp	Ref	Expression
1		fveqeq2	|- ( w = W -> ( ( # ` w ) = N <-> ( # ` W ) = N ) )
2		clwwlkn	|- ( N ClWWalksN G ) = { w e. ( ClWWalks ` G ) | ( # ` w ) = N }
3	1 2	elrab2	|- ( W e. ( N ClWWalksN G ) <-> ( W e. ( ClWWalks ` G ) /\ ( # ` W ) = N ) )