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 e. ( X ( ClWWalksNOn ` G ) N ) <-> ( W e. ( 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 e. ( N ClWWalksN G ) | ( w ` 0 ) = X }
4	2 3	elrab2	|- ( W e. ( X ( ClWWalksNOn ` G ) N ) <-> ( W e. ( N ClWWalksN G ) /\ ( W ` 0 ) = X ) )