Theorem clwwlknon2

Description: The set of closed walks on vertex X of length 2 in a graph G as words over the set of vertices. (Contributed by AV, 5-Mar-2022) (Revised by AV, 25-Mar-2022)

	Ref	Expression
Hypothesis	clwwlknon2.c	|- C = ( ClWWalksNOn ` G )
Assertion	clwwlknon2	|- ( X C 2 ) = { w e. ( 2 ClWWalksN G ) | ( w ` 0 ) = X }

Proof

Step	Hyp	Ref	Expression
1		clwwlknon2.c	|- C = ( ClWWalksNOn ` G )
2	1	oveqi	|- ( X C 2 ) = ( X ( ClWWalksNOn ` G ) 2 )
3		clwwlknon	|- ( X ( ClWWalksNOn ` G ) 2 ) = { w e. ( 2 ClWWalksN G ) | ( w ` 0 ) = X }
4	2 3	eqtri	|- ( X C 2 ) = { w e. ( 2 ClWWalksN G ) | ( w ` 0 ) = X }