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 eqtrid ⊢ V = ∅ → UnivVtx ⁡ G = ∅