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

Proof

Step	Hyp	Ref	Expression
1		fveq1	⊢ ( 𝑤 = 𝑊 → ( 𝑤 ‘ 0 ) = ( 𝑊 ‘ 0 ) )
2	1	eqeq1d	⊢ ( 𝑤 = 𝑊 → ( ( 𝑤 ‘ 0 ) = 𝑋 ↔ ( 𝑊 ‘ 0 ) = 𝑋 ) )
3		clwwlknon	⊢ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) = { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 }
4	2 3	elrab2	⊢ ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ↔ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) )