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 V

Proof

Step Hyp Ref Expression
1 uvtxel.v V = Vtx G
2 1 uvtxisvtx n UnivVtx G n V
3 2 ssriv UnivVtx G V