Metamath Proof Explorer

Theorem uvtxnbgrss

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)

Ref Expression
Hypothesis uvtxel.v ⊢ V = Vtx ⁡ G
Assertion uvtxnbgrss ⊢ N ∈ UnivVtx ⁡ G → V ∖ N ⊆ G NeighbVtx N

Proof

Step Hyp Ref Expression
1 uvtxel.v ⊢ V = Vtx ⁡ G
2 1 vtxnbuvtx ⊢ N ∈ UnivVtx ⁡ G → ∀ n ∈ V ∖ N n ∈ G NeighbVtx N
3 dfss3 ⊢ V ∖ N ⊆ G NeighbVtx N ↔ ∀ n ∈ V ∖ N n ∈ G NeighbVtx N
4 2 3 sylibr ⊢ N ∈ UnivVtx ⁡ G → V ∖ N ⊆ G NeighbVtx N