Metamath Proof Explorer

Theorem uvtxisvtx

Description: A universal vertex is a vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 30-Oct-2020) (Proof shortened by AV, 14-Feb-2022)

Ref Expression
Hypothesis uvtxel.v ⊢ V = Vtx ⁡ G
Assertion uvtxisvtx ⊢ N ∈ UnivVtx ⁡ G → N ∈ V

Proof

Step Hyp Ref Expression
1 uvtxel.v ⊢ V = Vtx ⁡ G
2 1 uvtxel ⊢ N ∈ UnivVtx ⁡ G ↔ N ∈ V ∧ ∀ n ∈ V ∖ N n ∈ G NeighbVtx N
3 2 simplbi ⊢ N ∈ UnivVtx ⁡ G → N ∈ V