Metamath Proof Explorer

Theorem uvtxssvtx

Description: The set of the universal vertices is a subset of the set of all vertices. (Contributed by AV, 23-Dec-2020)

Ref Expression
Hypothesis uvtxel.v 
|- V = ( Vtx ` G )
Assertion uvtxssvtx 
|- ( UnivVtx ` G ) C_ V

Proof

Step Hyp Ref Expression
1 uvtxel.v 
 |-  V = ( Vtx ` G )
2 1 uvtxisvtx 
 |-  ( n e. ( UnivVtx ` G ) -> n e. V )
3 2 ssriv 
 |-  ( UnivVtx ` G ) C_ V