Metamath Proof Explorer


Theorem uvtx0

Description: There is no universal vertex if there is no 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 uvtx0 V = UnivVtx G =

Proof

Step Hyp Ref Expression
1 uvtxel.v V = Vtx G
2 1 uvtxval UnivVtx G = v V | n V v n G NeighbVtx v
3 rabeq V = v V | n V v n G NeighbVtx v = v | n V v n G NeighbVtx v
4 rab0 v | n V v n G NeighbVtx v =
5 3 4 eqtrdi V = v V | n V v n G NeighbVtx v =
6 2 5 syl5eq V = UnivVtx G =