Metamath Proof Explorer

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 
|- V = ( Vtx ` G )
Assertion clnbgrssvtx 
|- ( G ClNeighbVtx K ) C_ V

Proof

Step Hyp Ref Expression
1 clnbgrvtxel.v 
 |-  V = ( Vtx ` G )
2 1 clnbgrisvtx 
 |-  ( n e. ( G ClNeighbVtx K ) -> n e. V )
3 2 ssriv 
 |-  ( G ClNeighbVtx K ) C_ V