This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝑋 ∉ ( 𝐺 NeighbVtx 𝑋 )

Proof

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