Metamath Proof Explorer

Theorem nbgrnself2

Description: A class X is not a neighbor of itself (whether it is a vertex or not). (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 3-Nov-2020) (Revised by AV, 12-Feb-2022)

Ref Expression
Assertion nbgrnself2 ⊢ X ∉ G NeighbVtx X

Proof

Step Hyp Ref Expression
1 id ⊢ v = X → v = X
2 oveq2 ⊢ v = X → G NeighbVtx v = G NeighbVtx X
3 1 2 neleq12d ⊢ v = X → v ∉ G NeighbVtx v ↔ X ∉ G NeighbVtx X
4 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
5 4 nbgrnself ⊢ ∀ v ∈ Vtx ⁡ G v ∉ G NeighbVtx v
6 3 5 vtoclri ⊢ X ∈ Vtx ⁡ G → X ∉ G NeighbVtx X
7 4 nbgrisvtx ⊢ X ∈ G NeighbVtx X → X ∈ Vtx ⁡ G
8 7 con3i ⊢ ¬ X ∈ Vtx ⁡ G → ¬ X ∈ G NeighbVtx X
9 df-nel ⊢ X ∉ G NeighbVtx X ↔ ¬ X ∈ G NeighbVtx X
10 8 9 sylibr ⊢ ¬ X ∈ Vtx ⁡ G → X ∉ G NeighbVtx X
11 6 10 pm2.61i ⊢ X ∉ G NeighbVtx X