Metamath Proof Explorer

Theorem nbgrssovtx

Description: The neighbors of a vertex X form a subset of all vertices except the vertex X itself. Stronger version of nbgrssvtx . (Contributed by Alexander van der Vekens, 13-Jul-2018) (Revised by AV, 3-Nov-2020) (Revised by AV, 12-Feb-2022)

Ref Expression
Hypothesis nbgrssovtx.v ⊢ V = Vtx ⁡ G
Assertion nbgrssovtx ⊢ G NeighbVtx X ⊆ V ∖ X

Proof

Step Hyp Ref Expression
1 nbgrssovtx.v ⊢ V = Vtx ⁡ G
2 1 nbgrisvtx ⊢ v ∈ G NeighbVtx X → v ∈ V
3 nbgrnself2 ⊢ X ∉ G NeighbVtx X
4 df-nel ⊢ v ∉ G NeighbVtx X ↔ ¬ v ∈ G NeighbVtx X
5 neleq1 ⊢ v = X → v ∉ G NeighbVtx X ↔ X ∉ G NeighbVtx X
6 4 5 bitr3id ⊢ v = X → ¬ v ∈ G NeighbVtx X ↔ X ∉ G NeighbVtx X
7 3 6 mpbiri ⊢ v = X → ¬ v ∈ G NeighbVtx X
8 7 necon2ai ⊢ v ∈ G NeighbVtx X → v ≠ X
9 eldifsn ⊢ v ∈ V ∖ X ↔ v ∈ V ∧ v ≠ X
10 2 8 9 sylanbrc ⊢ v ∈ G NeighbVtx X → v ∈ V ∖ X
11 10 ssriv ⊢ G NeighbVtx X ⊆ V ∖ X