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 𝑋 )