Metamath Proof Explorer

Theorem nbgrnself

Description: A vertex in a graph is not a neighbor of itself. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 3-Nov-2020) (Revised by AV, 21-Mar-2021)

Ref Expression
Hypothesis nbgrnself.v ⊢ V = Vtx ⁡ G
Assertion nbgrnself ⊢ ∀ v ∈ V v ∉ G NeighbVtx v

Proof

Step Hyp Ref Expression
1 nbgrnself.v ⊢ V = Vtx ⁡ G
2 neldifsnd ⊢ v ∈ V → ¬ v ∈ V ∖ v
3 2 intnanrd ⊢ v ∈ V → ¬ v ∈ V ∖ v ∧ ∃ e ∈ Edg ⁡ G v v ⊆ e
4 df-nel ⊢ v ∉ n ∈ V ∖ v | ∃ e ∈ Edg ⁡ G v n ⊆ e ↔ ¬ v ∈ n ∈ V ∖ v | ∃ e ∈ Edg ⁡ G v n ⊆ e
5 preq2 ⊢ n = v → v n = v v
6 5 sseq1d ⊢ n = v → v n ⊆ e ↔ v v ⊆ e
7 6 rexbidv ⊢ n = v → ∃ e ∈ Edg ⁡ G v n ⊆ e ↔ ∃ e ∈ Edg ⁡ G v v ⊆ e
8 7 elrab ⊢ v ∈ n ∈ V ∖ v | ∃ e ∈ Edg ⁡ G v n ⊆ e ↔ v ∈ V ∖ v ∧ ∃ e ∈ Edg ⁡ G v v ⊆ e
9 4 8 xchbinx ⊢ v ∉ n ∈ V ∖ v | ∃ e ∈ Edg ⁡ G v n ⊆ e ↔ ¬ v ∈ V ∖ v ∧ ∃ e ∈ Edg ⁡ G v v ⊆ e
10 3 9 sylibr ⊢ v ∈ V → v ∉ n ∈ V ∖ v | ∃ e ∈ Edg ⁡ G v n ⊆ e
11 eqidd ⊢ v ∈ V → v = v
12 eqid ⊢ Edg ⁡ G = Edg ⁡ G
13 1 12 nbgrval ⊢ v ∈ V → G NeighbVtx v = n ∈ V ∖ v | ∃ e ∈ Edg ⁡ G v n ⊆ e
14 11 13 neleq12d ⊢ v ∈ V → v ∉ G NeighbVtx v ↔ v ∉ n ∈ V ∖ v | ∃ e ∈ Edg ⁡ G v n ⊆ e
15 10 14 mpbird ⊢ v ∈ V → v ∉ G NeighbVtx v
16 15 rgen ⊢ ∀ v ∈ V v ∉ G NeighbVtx v