Theorem clnbgrssvtx

Description: The closed neighborhood of a vertex K in a graph is a subset of all vertices of the graph. (Contributed by AV, 9-May-2025)

	Ref	Expression
Hypothesis	clnbgrvtxel.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	clnbgrssvtx	⊢ ( 𝐺 ClNeighbVtx 𝐾 ) ⊆ 𝑉

Proof

Step	Hyp	Ref	Expression
1		clnbgrvtxel.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2	1	clnbgrisvtx	⊢ ( 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝐾 ) → 𝑛 ∈ 𝑉 )
3	2	ssriv	⊢ ( 𝐺 ClNeighbVtx 𝐾 ) ⊆ 𝑉