Metamath Proof Explorer


Theorem elclnbgrelnbgr

Description: An element of the closed neighborhood of a vertex which is not the vertex itself is an element of the open neighborhood of the vertex. (Contributed by AV, 24-Sep-2025)

Ref Expression
Assertion elclnbgrelnbgr X G ClNeighbVtx N X N X G NeighbVtx N

Proof

Step Hyp Ref Expression
1 eqid Vtx G = Vtx G
2 1 clnbgrcl X G ClNeighbVtx N N Vtx G
3 1 dfclnbgr4 N Vtx G G ClNeighbVtx N = N G NeighbVtx N
4 2 3 syl X G ClNeighbVtx N G ClNeighbVtx N = N G NeighbVtx N
5 4 eleq2d X G ClNeighbVtx N X G ClNeighbVtx N X N G NeighbVtx N
6 elun X N G NeighbVtx N X N X G NeighbVtx N
7 elsng X G ClNeighbVtx N X N X = N
8 eqneqall X = N X N X G NeighbVtx N
9 8 a1i X G ClNeighbVtx N X = N X N X G NeighbVtx N
10 7 9 sylbid X G ClNeighbVtx N X N X N X G NeighbVtx N
11 ax-1 X G NeighbVtx N X N X G NeighbVtx N
12 11 a1i X G ClNeighbVtx N X G NeighbVtx N X N X G NeighbVtx N
13 10 12 jaod X G ClNeighbVtx N X N X G NeighbVtx N X N X G NeighbVtx N
14 6 13 biimtrid X G ClNeighbVtx N X N G NeighbVtx N X N X G NeighbVtx N
15 5 14 sylbid X G ClNeighbVtx N X G ClNeighbVtx N X N X G NeighbVtx N
16 15 pm2.43i X G ClNeighbVtx N X N X G NeighbVtx N
17 16 imp X G ClNeighbVtx N X N X G NeighbVtx N