Metamath Proof Explorer


Theorem nbgrssvtx

Description: The neighbors of a vertex K in a graph form a subset of all vertices of the graph. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 26-Oct-2020) (Revised by AV, 12-Feb-2022)

Ref Expression
Hypothesis nbgrisvtx.v
|- V = ( Vtx ` G )
Assertion nbgrssvtx
|- ( G NeighbVtx K ) C_ V

Proof

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