Metamath Proof Explorer


Theorem clnbgrnvtx0

Description: If a class X is not a vertex of a graph G , then it has an empty closed neighborhood in G . (Contributed by AV, 8-May-2025)

Ref Expression
Hypothesis clnbgrel.v V = Vtx G
Assertion clnbgrnvtx0 X V G ClNeighbVtx X =

Proof

Step Hyp Ref Expression
1 clnbgrel.v V = Vtx G
2 csbfv G / g Vtx g = Vtx G
3 1 2 eqtr4i V = G / g Vtx g
4 neleq2 V = G / g Vtx g X V X G / g Vtx g
5 3 4 ax-mp X V X G / g Vtx g
6 5 biimpi X V X G / g Vtx g
7 6 olcd X V G V X G / g Vtx g
8 df-clnbgr ClNeighbVtx = g V , v Vtx g v n Vtx g | e Edg g v n e
9 8 mpoxneldm G V X G / g Vtx g G ClNeighbVtx X =
10 7 9 syl X V G ClNeighbVtx X =