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=\mathrm{ClWWalksNOn}\left(G\right)$$
Assertion	clwwlknon2	$$⊢XC2=\left\{w\in \left(2\mathrm{ClWWalksN}G\right)|w\left(0\right)=X\right\}$$

Proof

Step	Hyp	Ref	Expression
1		clwwlknon2.c	$$⊢C=\mathrm{ClWWalksNOn}\left(G\right)$$
2	1	oveqi	$$⊢XC2=X\mathrm{ClWWalksNOn}\left(G\right)2$$
3		clwwlknon	$$⊢X\mathrm{ClWWalksNOn}\left(G\right)2=\left\{w\in \left(2\mathrm{ClWWalksN}G\right)|w\left(0\right)=X\right\}$$
4	2 3	eqtri	$$⊢XC2=\left\{w\in \left(2\mathrm{ClWWalksN}G\right)|w\left(0\right)=X\right\}$$