Metamath Proof Explorer


Theorem vtxnbuvtx

Description: A universal vertex has all other vertices as neighbors. (Contributed by Alexander van der Vekens, 14-Oct-2017) (Revised by AV, 30-Oct-2020) (Proof shortened by AV, 14-Feb-2022)

Ref Expression
Hypothesis uvtxel.v V = Vtx G
Assertion vtxnbuvtx N UnivVtx G n V N n G NeighbVtx N

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 simprbi N UnivVtx G n V N n G NeighbVtx N