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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	uvtxssvtx	⊢ ( UnivVtx ‘ 𝐺 ) ⊆ 𝑉

Proof

Step	Hyp	Ref	Expression
1		uvtxel.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2	1	uvtxisvtx	⊢ ( 𝑛 ∈ ( UnivVtx ‘ 𝐺 ) → 𝑛 ∈ 𝑉 )
3	2	ssriv	⊢ ( UnivVtx ‘ 𝐺 ) ⊆ 𝑉